Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### 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