Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### The Modification of a Function by a Function and the Iteration of the Composition of a Function

**by****Czeslaw Bylinski**- Received March 1, 1990
- MML identifier: FUNCT_4

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, TARSKI, RELAT_1, BOOLE, FUNCOP_1, PARTFUN1, FUNCT_2, FUNCT_4; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, PARTFUN1, FUNCOP_1; constructors PARTFUN1, FUNCOP_1, TARSKI, XBOOLE_0; clusters RELAT_1, FUNCT_1, RELSET_1, XBOOLE_0, FUNCOP_1, ZFMISC_1; requirements BOOLE, SUBSET; begin reserve a,b,p,x,x',x1,x1',x2,y,y',y1,y1',y2,z,z',z1,z2,X,X',Y,Y',Z,Z' for set; reserve A,D,D' for non empty set; reserve f,g,h for Function; theorem :: FUNCT_4:1 (for z st z in Z holds ex x,y st z = [x,y]) implies ex X,Y st Z c= [:X,Y:]; theorem :: FUNCT_4:2 g*f = (g|rng f)*f; theorem :: FUNCT_4:3 {} = {} --> a; theorem :: FUNCT_4:4 id X c= id Y iff X c= Y; theorem :: FUNCT_4:5 X c= Y implies X --> a c= Y --> a; theorem :: FUNCT_4:6 X --> a c= Y --> b implies X c= Y; theorem :: FUNCT_4:7 X <> {} & X --> a c= Y --> b implies a = b; theorem :: FUNCT_4:8 x in dom f implies {x} --> f.x c= f; :: Natural order on functions definition let f,g; redefine pred f c= g; synonym f <= g; end; theorem :: FUNCT_4:9 Y|f|X <= f; theorem :: FUNCT_4:10 f <= g implies Y|f|X <= Y|g|X; definition let f,g; func f +* g -> Function means :: FUNCT_4:def 1 dom it = dom f \/ dom g & for x st x in dom f \/ dom g holds (x in dom g implies it.x = g.x) & (not x in dom g implies it.x = f.x); idempotence; end; theorem :: FUNCT_4:11 dom f c= dom(f+*g) & dom g c= dom(f+*g); theorem :: FUNCT_4:12 not x in dom g implies (f +* g).x = f.x; theorem :: FUNCT_4:13 x in dom(f +* g) iff x in dom f or x in dom g; theorem :: FUNCT_4:14 x in dom g implies (f+*g).x = g.x; theorem :: FUNCT_4:15 f +* g +* h = f +* (g +* h); theorem :: FUNCT_4:16 f tolerates g & x in dom f implies (f+*g).x = f.x; theorem :: FUNCT_4:17 dom f misses dom g & x in dom f implies (f +* g).x = f.x; theorem :: FUNCT_4:18 rng(f +* g) c= rng f \/ rng g; theorem :: FUNCT_4:19 rng g c= rng(f +* g); theorem :: FUNCT_4:20 dom f c= dom g implies f +* g = g; theorem :: FUNCT_4:21 {} +* f = f; theorem :: FUNCT_4:22 f +* {} = f; theorem :: FUNCT_4:23 id(X) +* id(Y) = id(X \/ Y); theorem :: FUNCT_4:24 (f +* g)|(dom g) = g; theorem :: FUNCT_4:25 ((f +* g)|(dom f \ dom g)) c= f; theorem :: FUNCT_4:26 g c= (f +* g); theorem :: FUNCT_4:27 f tolerates g +* h implies f|(dom f \ dom h) tolerates g; theorem :: FUNCT_4:28 f tolerates g +* h implies f tolerates h; theorem :: FUNCT_4:29 f tolerates g iff f c= f +* g; theorem :: FUNCT_4:30 f +* g c= f \/ g; theorem :: FUNCT_4:31 f tolerates g iff f \/ g = f +* g; theorem :: FUNCT_4:32 dom f misses dom g implies f \/ g = f +* g; theorem :: FUNCT_4:33 dom f misses dom g implies f c= f +* g; theorem :: FUNCT_4:34 dom f misses dom g implies (f +* g)|(dom f) = f; theorem :: FUNCT_4:35 f tolerates g iff f +* g = g +* f; theorem :: FUNCT_4:36 dom f misses dom g implies f +* g = g +* f; theorem :: FUNCT_4:37 for f,g being PartFunc of X,Y st g is total holds f +* g = g; theorem :: FUNCT_4:38 for f,g being Function of X,Y st Y = {} implies X = {} holds f +* g = g; theorem :: FUNCT_4:39 for f,g being Function of X,X holds f +* g = g; theorem :: FUNCT_4:40 for f,g being Function of X,D holds f +* g = g; theorem :: FUNCT_4:41 for f,g being PartFunc of X,Y holds f +* g is PartFunc of X,Y; :: The converse function whenever domain definition let f; func ~f -> Function means :: FUNCT_4:def 2 (for x holds x in dom it iff ex y,z st x = [z,y] & [y,z] in dom f) & (for y,z st [y,z] in dom f holds it.[z,y] = f.[y,z]); end; theorem :: FUNCT_4:42 rng ~f c= rng f; theorem :: FUNCT_4:43 [x,y] in dom f iff [y,x] in dom ~f; theorem :: FUNCT_4:44 [y,x] in dom ~f implies (~f).[y,x] = f.[x,y]; theorem :: FUNCT_4:45 ex X,Y st dom ~f c= [:X,Y:]; theorem :: FUNCT_4:46 dom f c= [:X,Y:] implies dom ~f c= [:Y,X:]; theorem :: FUNCT_4:47 dom f = [:X,Y:] implies dom ~f = [:Y,X:]; theorem :: FUNCT_4:48 dom f c= [:X,Y:] implies rng ~f = rng f; theorem :: FUNCT_4:49 for f being PartFunc of [:X,Y:],Z holds ~f is PartFunc of [:Y,X:],Z; theorem :: FUNCT_4:50 for f being Function of [:X,Y:],Z st Z<>{} holds ~f is Function of [:Y,X:],Z ; theorem :: FUNCT_4:51 for f being Function of [:X,Y:],D holds ~f is Function of [:Y,X:],D ; theorem :: FUNCT_4:52 ~~f c= f; theorem :: FUNCT_4:53 dom f c= [:X,Y:] implies ~~f = f; theorem :: FUNCT_4:54 for f being PartFunc of [:X,Y:],Z holds ~~f = f; theorem :: FUNCT_4:55 for f being Function of [:X,Y:],Z st Z <> {} holds ~~f = f; theorem :: FUNCT_4:56 for f being Function of [:X,Y:],D holds ~~f = f; :: Product of 2'ary functions definition let f,g; func |:f,g:| -> Function means :: FUNCT_4:def 3 (for z holds z in dom it iff ex x,y,x',y' st z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g) & (for x,y,x',y' st [x,y] in dom f & [x',y'] in dom g holds it.[[x,x'],[y,y']] = [f.[x,y],g.[x',y']]); end; theorem :: FUNCT_4:57 [[x,x'],[y,y']] in dom |:f,g:| iff [x,y] in dom f & [x',y'] in dom g; theorem :: FUNCT_4:58 [[x,x'],[y,y']] in dom |:f,g:| implies |:f,g:|.[[x,x'],[y,y']] = [f.[x,y],g.[x',y']]; theorem :: FUNCT_4:59 rng |:f,g:| c= [:rng f,rng g:]; theorem :: FUNCT_4:60 dom f c= [:X,Y:] & dom g c= [:X',Y':] implies dom|:f,g:| c= [:[:X,X':],[:Y,Y':]:]; theorem :: FUNCT_4:61 dom f = [:X,Y:] & dom g = [:X',Y':] implies dom|:f,g:| = [:[:X,X':],[:Y,Y':]:]; theorem :: FUNCT_4:62 for f being PartFunc of [:X,Y:],Z for g being PartFunc of [:X',Y':],Z' holds |:f,g:| is PartFunc of [:[:X,X':],[:Y,Y':]:],[:Z,Z':]; theorem :: FUNCT_4:63 for f being Function of [:X,Y:],Z for g being Function of [:X',Y':],Z' st Z <> {} & Z' <> {} holds |:f,g:| is Function of [:[:X,X':],[:Y,Y':]:],[:Z,Z':]; theorem :: FUNCT_4:64 for f being Function of [:X,Y:],D for g being Function of [:X',Y':],D' holds |:f,g:| is Function of [:[:X,X':],[:Y,Y':]:],[:D,D':]; definition let x,y,a,b be set; func (x,y) --> (a,b) -> set equals :: FUNCT_4:def 4 ({x} --> a) +* ({y} --> b); end; definition let x,y,a,b be set; cluster (x,y) --> (a,b) -> Function-like Relation-like; end; theorem :: FUNCT_4:65 dom((x1,x2) --> (y1,y2)) = {x1,x2} & rng((x1,x2) --> (y1,y2)) c= {y1,y2}; theorem :: FUNCT_4:66 x1 <> x2 implies ((x1,x2) --> (y1,y2)).x1 = y1 & ((x1,x2) --> (y1,y2)).x2 = y2; theorem :: FUNCT_4:67 x1 <> x2 implies rng((x1,x2) --> (y1,y2)) = {y1,y2}; theorem :: FUNCT_4:68 (x1,x2) --> (y,y) = {x1,x2} --> y; definition let A,x1,x2; let y1,y2 be Element of A; redefine func (x1,x2) --> (y1,y2) -> Function of {x1,x2},A; end; theorem :: FUNCT_4:69 for a,b,c,d being set, g being Function st dom g = {a,b} & g.a = c & g.b = d holds g = (a,b) --> (c,d); theorem :: FUNCT_4:70 for x,y being set holds {x} --> y = {[x,y]}; theorem :: FUNCT_4:71 for a,b,c,d being set st a <> c holds (a,c) --> (b,d) = { [a,b], [c,d] }; theorem :: FUNCT_4:72 for a,b,x,y,x',y' being set st a <> b & (a,b) --> (x,y) = (a,b) --> (x',y') holds x = x' & y = y';

Back to top