Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Functions and Their Basic Properties

**by****Czeslaw Bylinski**- Received March 3, 1989
- MML identifier: FUNCT_1

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_1, BOOLE, FUNCT_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1; constructors TARSKI, RELAT_1, SUBSET_1, XBOOLE_0; clusters SUBSET_1, RELAT_1, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin reserve X,X1,X2,Y,Y1,Y2 for set, p,x,x1,x2,y,y1,y2,z,z1,z2 for set; definition let X be set; attr X is Function-like means :: FUNCT_1:def 1 for x,y1,y2 st [x,y1] in X & [x,y2] in X holds y1 = y2; end; definition cluster Relation-like Function-like set; end; definition mode Function is Function-like Relation-like set; end; definition cluster empty -> Function-like set; end; reserve f,g,g1,g2,h for Function, R,S for Relation; canceled; theorem :: FUNCT_1:2 for F being set st (for p st p in F ex x,y st [x,y] = p) & (for x,y1,y2 st [x,y1] in F & [x,y2] in F holds y1 = y2) holds F is Function; scheme GraphFunc{A()->set,P[set,set]}: ex f st for x,y holds [x,y] in f iff x in A() & P[x,y] provided for x,y1,y2 st P[x,y1] & P[x,y2] holds y1 = y2; definition let f,x; canceled 2; func f.x -> set means :: FUNCT_1:def 4 [x,it] in f if x in dom f otherwise it = {}; end; canceled 5; theorem :: FUNCT_1:8 [x,y] in f iff x in dom f & y = f.x; theorem :: FUNCT_1:9 dom f = dom g & (for x st x in dom f holds f.x = g.x) implies f = g; definition let f; redefine func rng f means :: FUNCT_1:def 5 for y holds y in it iff ex x st x in dom f & y = f.x; end; canceled 2; theorem :: FUNCT_1:12 x in dom f implies f.x in rng f; canceled; theorem :: FUNCT_1:14 dom f = {x} implies rng f = {f.x}; scheme FuncEx{A()->set,P[set,set]}: ex f st dom f = A() & for x st x in A() holds P[x,f.x] provided for x,y1,y2 st x in A() & P[x,y1] & P[x,y2] holds y1 = y2 and for x st x in A() ex y st P[x,y]; scheme Lambda{A()->set,F(set)->set}: ex f being Function st dom f = A() & for x st x in A() holds f.x = F(x); theorem :: FUNCT_1:15 X <> {} implies for y ex f st dom f = X & rng f = {y}; theorem :: FUNCT_1:16 (for f,g st dom f = X & dom g = X holds f = g) implies X = {}; theorem :: FUNCT_1:17 dom f = dom g & rng f = {y} & rng g = {y} implies f = g; theorem :: FUNCT_1:18 Y <> {} or X = {} implies ex f st X = dom f & rng f c= Y; theorem :: FUNCT_1:19 (for y st y in Y ex x st x in dom f & y = f.x) implies Y c= rng f; definition let f,g; redefine func f*g; synonym g*f; end; definition let f,g; cluster g*f -> Function-like; end; theorem :: FUNCT_1:20 for h st (for x holds x in dom h iff x in dom f & f.x in dom g) & (for x st x in dom h holds h.x = g.(f.x)) holds h = g*f; theorem :: FUNCT_1:21 x in dom(g*f) iff x in dom f & f.x in dom g; theorem :: FUNCT_1:22 x in dom(g*f) implies (g*f).x = g.(f.x); theorem :: FUNCT_1:23 x in dom f implies (g*f).x = g.(f.x); canceled; theorem :: FUNCT_1:25 z in rng(g*f) implies z in rng g; canceled; theorem :: FUNCT_1:27 dom(g*f) = dom f implies rng f c= dom g; canceled 5; theorem :: FUNCT_1:33 rng f c= Y & (for g,h st dom g = Y & dom h = Y & g*f = h*f holds g = h) implies Y = rng f; definition let X; cluster id X -> Function-like; end; theorem :: FUNCT_1:34 f = id X iff dom f = X & for x st x in X holds f.x = x; theorem :: FUNCT_1:35 x in X implies (id X).x = x; canceled; theorem :: FUNCT_1:37 dom(f*(id X)) = dom f /\ X; theorem :: FUNCT_1:38 x in dom f /\ X implies f.x = (f*(id X)).x; canceled; theorem :: FUNCT_1:40 x in dom((id Y)*f) iff x in dom f & f.x in Y; canceled; theorem :: FUNCT_1:42 f*(id dom f) = f & (id rng f)*f = f; theorem :: FUNCT_1:43 (id X)*(id Y) = id(X /\ Y); theorem :: FUNCT_1:44 rng f = dom g & g*f = f implies g = id dom g; definition let f; canceled 2; attr f is one-to-one means :: FUNCT_1:def 8 for x1,x2 st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2; end; canceled; theorem :: FUNCT_1:46 f is one-to-one & g is one-to-one implies g*f is one-to-one; theorem :: FUNCT_1:47 g*f is one-to-one & rng f c= dom g implies f is one-to-one; theorem :: FUNCT_1:48 g*f is one-to-one & rng f = dom g implies f is one-to-one & g is one-to-one; theorem :: FUNCT_1:49 f is one-to-one iff (for g,h st rng g c= dom f & rng h c= dom f & dom g = dom h & f*g = f*h holds g = h); theorem :: FUNCT_1:50 dom f = X & dom g = X & rng g c= X & f is one-to-one & f*g = f implies g = id X; theorem :: FUNCT_1:51 rng(g*f) = rng g & g is one-to-one implies dom g c= rng f; theorem :: FUNCT_1:52 id X is one-to-one; theorem :: FUNCT_1:53 (ex g st g*f = id dom f) implies f is one-to-one; definition cluster empty Function; end; definition cluster empty -> one-to-one Function; end; definition cluster one-to-one Function; end; definition let f be one-to-one Function; cluster f~ -> Function-like; end; definition let f; assume f is one-to-one; func f" -> Function equals :: FUNCT_1:def 9 f~; end; theorem :: FUNCT_1:54 f is one-to-one implies for g being Function holds g=f" iff dom g = rng f & for y,x holds y in rng f & x = g.y iff x in dom f & y = f.x; theorem :: FUNCT_1:55 f is one-to-one implies rng f = dom(f") & dom f = rng(f"); theorem :: FUNCT_1:56 f is one-to-one & x in dom f implies x = (f").(f.x) & x = (f"*f).x; theorem :: FUNCT_1:57 f is one-to-one & y in rng f implies y = f.((f").y) & y = (f*f").y; theorem :: FUNCT_1:58 f is one-to-one implies dom(f"*f) = dom f & rng(f"*f) = dom f; theorem :: FUNCT_1:59 f is one-to-one implies dom(f*f") = rng f & rng(f*f") = rng f; theorem :: FUNCT_1:60 f is one-to-one & dom f = rng g & rng f = dom g & (for x,y st x in dom f & y in dom g holds f.x = y iff g.y = x) implies g = f"; theorem :: FUNCT_1:61 f is one-to-one implies f"*f = id dom f & f*f" = id rng f; theorem :: FUNCT_1:62 f is one-to-one implies f" is one-to-one; theorem :: FUNCT_1:63 f is one-to-one & rng f = dom g & g*f = id dom f implies g = f"; theorem :: FUNCT_1:64 f is one-to-one & rng g = dom f & f*g = id rng f implies g = f"; theorem :: FUNCT_1:65 f is one-to-one implies (f")" = f; theorem :: FUNCT_1:66 f is one-to-one & g is one-to-one implies (g*f)" = f"*g"; theorem :: FUNCT_1:67 (id X)" = (id X); definition let f,X; cluster f|X -> Function-like; end; theorem :: FUNCT_1:68 g = f|X iff dom g = dom f /\ X & for x st x in dom g holds g.x = f.x; canceled; theorem :: FUNCT_1:70 x in dom(f|X) implies (f|X).x = f.x; theorem :: FUNCT_1:71 x in dom f /\ X implies (f|X).x = f.x; theorem :: FUNCT_1:72 x in X implies (f|X).x = f.x; theorem :: FUNCT_1:73 x in dom f & x in X implies f.x in rng(f|X); canceled 2; theorem :: FUNCT_1:76 dom(f|X) c= dom f & rng(f|X) c= rng f; canceled 5; theorem :: FUNCT_1:82 X c= Y implies (f|X)|Y = f|X & (f|Y)|X = f|X; canceled; theorem :: FUNCT_1:84 f is one-to-one implies f|X is one-to-one; definition let Y,f; cluster Y|f -> Function-like; end; theorem :: FUNCT_1:85 g = Y|f iff (for x holds x in dom g iff x in dom f & f.x in Y) & (for x st x in dom g holds g.x = f.x); theorem :: FUNCT_1:86 x in dom(Y|f) iff x in dom f & f.x in Y; theorem :: FUNCT_1:87 x in dom(Y|f) implies (Y|f).x = f.x; canceled; theorem :: FUNCT_1:89 dom(Y|f) c= dom f & rng(Y|f) c= rng f; canceled 7; theorem :: FUNCT_1:97 X c= Y implies Y|(X|f) = X|f & X|(Y|f) = X|f; canceled; theorem :: FUNCT_1:99 f is one-to-one implies Y|f is one-to-one; definition let f,X; redefine canceled 2; func f.:X means :: FUNCT_1:def 12 for y holds y in it iff ex x st x in dom f & x in X & y = f.x; end; canceled 17; theorem :: FUNCT_1:117 x in dom f implies f.:{x} = {f.x}; theorem :: FUNCT_1:118 x1 in dom f & x2 in dom f implies f.:{x1,x2} = {f.x1,f.x2}; canceled; theorem :: FUNCT_1:120 (Y|f).:X c= f.:X; theorem :: FUNCT_1:121 f is one-to-one implies f.:(X1 /\ X2) = f.:X1 /\ f.:X2; theorem :: FUNCT_1:122 (for X1,X2 holds f.:(X1 /\ X2) = f.:X1 /\ f.:X2) implies f is one-to-one; theorem :: FUNCT_1:123 f is one-to-one implies f.:(X1 \ X2) = f.:X1 \ f.:X2; theorem :: FUNCT_1:124 (for X1,X2 holds f.:(X1 \ X2) = f.:X1 \ f.:X2) implies f is one-to-one; theorem :: FUNCT_1:125 X misses Y & f is one-to-one implies f.:X misses f.:Y; theorem :: FUNCT_1:126 (Y|f).:X = Y /\ f.:X; definition let f,Y; redefine func f"Y means :: FUNCT_1:def 13 for x holds x in it iff x in dom f & f.x in Y; end; canceled 10; theorem :: FUNCT_1:137 f"(Y1 /\ Y2) = f"Y1 /\ f"Y2; theorem :: FUNCT_1:138 f"(Y1 \ Y2) = f"Y1 \ f"Y2; theorem :: FUNCT_1:139 (R|X)"Y = X /\ (R"Y); canceled 2; theorem :: FUNCT_1:142 y in rng R iff R"{y} <> {}; theorem :: FUNCT_1:143 (for y st y in Y holds R"{y} <> {}) implies Y c= rng R; theorem :: FUNCT_1:144 (for y st y in rng f ex x st f"{y} = {x}) iff f is one-to-one; theorem :: FUNCT_1:145 f.:(f"Y) c= Y; theorem :: FUNCT_1:146 X c= dom R implies X c= R"(R.:X); theorem :: FUNCT_1:147 Y c= rng f implies f.:(f"Y) = Y; theorem :: FUNCT_1:148 f.:(f"Y) = Y /\ f.:(dom f); theorem :: FUNCT_1:149 f.:(X /\ f"Y) c= (f.:X) /\ Y; theorem :: FUNCT_1:150 f.:(X /\ f"Y) = (f.:X) /\ Y; theorem :: FUNCT_1:151 X /\ R"Y c= R"(R.:X /\ Y); theorem :: FUNCT_1:152 f is one-to-one implies f"(f.:X) c= X; theorem :: FUNCT_1:153 (for X holds f"(f.:X) c= X) implies f is one-to-one; theorem :: FUNCT_1:154 f is one-to-one implies f.:X = (f")"X; theorem :: FUNCT_1:155 f is one-to-one implies f"Y = (f").:Y; :: SUPLEMENT theorem :: FUNCT_1:156 Y = rng f & dom g = Y & dom h = Y & g*f = h*f implies g = h; theorem :: FUNCT_1:157 f.:X1 c= f.:X2 & X1 c= dom f & f is one-to-one implies X1 c= X2; theorem :: FUNCT_1:158 f"Y1 c= f"Y2 & Y1 c= rng f implies Y1 c= Y2; theorem :: FUNCT_1:159 f is one-to-one iff for y ex x st f"{y} c= {x}; theorem :: FUNCT_1:160 rng R c= dom S implies R"X c= (R*S)"(S.:X);

Back to top