:: Graphs of Functions
:: by Czes{\l}aw Byli\'nski
::
:: Received April 14, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem :: GRFUNC_1:1
canceled;
theorem :: GRFUNC_1:2
canceled;
theorem :: GRFUNC_1:3
canceled;
theorem :: GRFUNC_1:4
canceled;
theorem :: GRFUNC_1:5
canceled;
theorem Th6: :: GRFUNC_1:6
theorem :: GRFUNC_1:7
canceled;
theorem Th8: :: GRFUNC_1:8
theorem :: GRFUNC_1:9
Lm1:
for x, y being set
for f, h being Function st (rng f) /\ (rng h) = {} & x in dom f & y in dom h holds
f . x <> h . y
theorem :: GRFUNC_1:10
canceled;
theorem :: GRFUNC_1:11
canceled;
theorem :: GRFUNC_1:12
theorem :: GRFUNC_1:13
theorem :: GRFUNC_1:14
canceled;
theorem :: GRFUNC_1:15
Lm2:
for x, y, x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )
theorem :: GRFUNC_1:16
theorem :: GRFUNC_1:17
canceled;
theorem Th18: :: GRFUNC_1:18
theorem :: GRFUNC_1:19
for
x1,
y1,
x2,
y2 being
set holds
(
{[x1,y1],[x2,y2]} is
Function iff (
x1 = x2 implies
y1 = y2 ) )
theorem :: GRFUNC_1:20
canceled;
theorem :: GRFUNC_1:21
canceled;
theorem :: GRFUNC_1:22
canceled;
theorem :: GRFUNC_1:23
canceled;
theorem :: GRFUNC_1:24
canceled;
theorem Th25: :: GRFUNC_1:25
theorem Th26: :: GRFUNC_1:26
theorem :: GRFUNC_1:27
theorem :: GRFUNC_1:28
theorem :: GRFUNC_1:29
theorem :: GRFUNC_1:30
theorem :: GRFUNC_1:31
theorem :: GRFUNC_1:32
Lm3:
for x being set
for h, f, g being Function st h = f \/ g holds
( x in dom h iff ( x in dom f or x in dom g ) )
theorem :: GRFUNC_1:33
theorem Th34: :: GRFUNC_1:34
theorem :: GRFUNC_1:35
theorem :: GRFUNC_1:36
theorem :: GRFUNC_1:37
theorem :: GRFUNC_1:38
theorem :: GRFUNC_1:39
canceled;
theorem :: GRFUNC_1:40
canceled;
theorem :: GRFUNC_1:41
canceled;
theorem :: GRFUNC_1:42
canceled;
theorem :: GRFUNC_1:43
canceled;
theorem :: GRFUNC_1:44
canceled;
theorem :: GRFUNC_1:45
canceled;
theorem :: GRFUNC_1:46
theorem :: GRFUNC_1:47
theorem :: GRFUNC_1:48
canceled;
theorem :: GRFUNC_1:49
theorem :: GRFUNC_1:50
canceled;
theorem :: GRFUNC_1:51
canceled;
theorem :: GRFUNC_1:52
theorem :: GRFUNC_1:53
canceled;
theorem :: GRFUNC_1:54
canceled;
theorem :: GRFUNC_1:55
canceled;
theorem :: GRFUNC_1:56
canceled;
theorem :: GRFUNC_1:57
canceled;
theorem :: GRFUNC_1:58
canceled;
theorem :: GRFUNC_1:59
canceled;
theorem :: GRFUNC_1:60
canceled;
theorem :: GRFUNC_1:61
canceled;
theorem :: GRFUNC_1:62
canceled;
theorem :: GRFUNC_1:63
canceled;
theorem Th64: :: GRFUNC_1:64
theorem :: GRFUNC_1:65
canceled;
theorem :: GRFUNC_1:66
canceled;
theorem :: GRFUNC_1:67
theorem :: GRFUNC_1:68
canceled;
theorem :: GRFUNC_1:69
canceled;
theorem :: GRFUNC_1:70
canceled;
theorem :: GRFUNC_1:71
canceled;
theorem :: GRFUNC_1:72
canceled;
theorem :: GRFUNC_1:73
canceled;
theorem :: GRFUNC_1:74
canceled;
theorem :: GRFUNC_1:75
canceled;
theorem :: GRFUNC_1:76
canceled;
theorem :: GRFUNC_1:77
canceled;
theorem :: GRFUNC_1:78
canceled;
theorem :: GRFUNC_1:79
theorem :: GRFUNC_1:80
canceled;
theorem :: GRFUNC_1:81
canceled;
theorem :: GRFUNC_1:82
canceled;
theorem :: GRFUNC_1:83
canceled;
theorem :: GRFUNC_1:84
canceled;
theorem :: GRFUNC_1:85
canceled;
theorem :: GRFUNC_1:86
canceled;
theorem :: GRFUNC_1:87
theorem :: GRFUNC_1:88
theorem Th89: :: GRFUNC_1:89
theorem Th90: :: GRFUNC_1:90
theorem Th91: :: GRFUNC_1:91
theorem :: GRFUNC_1:92
theorem :: GRFUNC_1:93
theorem :: GRFUNC_1:94
theorem :: GRFUNC_1:95