Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Graphs of Functions

by
Czeslaw Bylinski

Received April 14, 1989

MML identifier: GRFUNC_1
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, RELAT_1, BOOLE;
notation TARSKI, XBOOLE_0, RELAT_1, FUNCT_1;
constructors TARSKI, SUBSET_1, FUNCT_1, XBOOLE_0;
clusters FUNCT_1, XBOOLE_0, ZFMISC_1;
requirements SUBSET, BOOLE;

begin

reserve X,Y,p,x,x1,x2,y,y1,y2,z,z1,z2 for set;
reserve f,g,h for Function;

canceled 5;

theorem :: GRFUNC_1:6
for G being set st G c= f holds G is Function;

canceled;

theorem :: GRFUNC_1:8
f c= g iff
dom f c= dom g & (for x st x in dom f holds f.x = g.x);

theorem :: GRFUNC_1:9
dom f = dom g & f c= g implies f = g;

canceled 2;

theorem :: GRFUNC_1:12
[x,z] in (g*f) implies [x,f.x] in f & [f.x,z] in g;

theorem :: GRFUNC_1:13
h c= f implies g*h c= g*f & h*g c= f*g;

canceled;

theorem :: GRFUNC_1:15
{[x,y]} is Function;

theorem :: GRFUNC_1:16
f = {[x,y]} implies f.x = y;

canceled;

theorem :: GRFUNC_1:18
dom f = {x} implies f = {[x,f.x]};

theorem :: GRFUNC_1:19
{[x1,y1],[x2,y2]} is Function iff (x1 = x2 implies y1 = y2);

canceled 5;

theorem :: GRFUNC_1:25
f is one-to-one iff
for x1,x2,y st [x1,y] in f & [x2,y] in f holds x1 = x2;

theorem :: GRFUNC_1:26
g c= f & f is one-to-one implies g is one-to-one;

theorem :: GRFUNC_1:27
f /\ X is Function & X /\ f is Function;

theorem :: GRFUNC_1:28
h = f /\ g
implies dom h c= dom f /\ dom g & rng h c= rng f /\ rng g;

theorem :: GRFUNC_1:29
h = f /\ g & x in dom h implies h.x = f.x & h.x = g.x;

theorem :: GRFUNC_1:30
(f is one-to-one or g is one-to-one) & h = f /\ g
implies h is one-to-one;

theorem :: GRFUNC_1:31
dom f misses dom g implies f \/ g is Function;

theorem :: GRFUNC_1:32
f c= h & g c= h implies f \/ g is Function;

theorem :: GRFUNC_1:33
h = f \/ g implies dom h = dom f \/ dom g & rng h = rng f \/ rng g;

theorem :: GRFUNC_1:34
x in dom f & h = f \/ g implies h.x = f.x;

theorem :: GRFUNC_1:35
x in dom g & h = f \/ g implies h.x = g.x;

theorem :: GRFUNC_1:36
x in dom h & h = f \/ g implies h.x = f.x or h.x = g.x;

theorem :: GRFUNC_1:37
f is one-to-one & g is one-to-one & h = f \/ g & rng f misses rng g
implies h is one-to-one;

theorem :: GRFUNC_1:38
f \ X is Function;

canceled 7;

theorem :: GRFUNC_1:46
f = {} implies f is one-to-one;

theorem :: GRFUNC_1:47
f is one-to-one implies for x,y holds [y,x] in f" iff [x,y] in f;

canceled;

theorem :: GRFUNC_1:49
f = {} implies f" = {};

canceled 2;

theorem :: GRFUNC_1:52
x in dom f & x in X iff [x,f.x] in f|X;

canceled;

theorem :: GRFUNC_1:54
((f|X)*h) c= (f*h) & (g*(f|X)) c= (g*f);

canceled 9;

theorem :: GRFUNC_1:64
g c= f implies f|dom g = g;

canceled 2;

theorem :: GRFUNC_1:67
x in dom f & f.x in Y iff [x,f.x] in Y|f;

canceled;

theorem :: GRFUNC_1:69
((Y|f)*h) c= (f*h) & (g*(Y|f)) c= (g*f);

canceled 9;

theorem :: GRFUNC_1:79
g c= f & f is one-to-one implies rng g|f = g;

canceled 7;

theorem :: GRFUNC_1:87
x in f"Y iff [x,f.x] in f & f.x in Y;

```

Back to top