Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### Cartesian Product of Functions

**by****Grzegorz Bancerek**- Received September 30, 1991
- MML identifier: FUNCT_6

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, FUNCT_2, CARD_3, FINSEQ_1, RELAT_1, FINSEQ_2, FUNCOP_1, PROB_1, TARSKI, FUNCT_5, BOOLE, PARTFUN1, SETFAM_1, FINSEQ_4, MCART_1, FUNCT_6; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, NAT_1, RELAT_1, FUNCT_1, MCART_1, FINSEQ_1, SETFAM_1, FUNCT_2, PARTFUN1, FUNCT_3, WELLORD2, FUNCOP_1, FINSEQ_2, FUNCT_4, FUNCT_5, PROB_1, CARD_3; constructors ENUMSET1, MCART_1, PARTFUN1, FUNCT_3, WELLORD2, FUNCOP_1, PROB_1, FINSEQ_2, FUNCT_4, FUNCT_5, CARD_3, XBOOLE_0; clusters SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, FINSEQ_1, RELSET_1, ARYTM_3, FUNCT_2, ZFMISC_1, XBOOLE_0; requirements NUMERALS, BOOLE, SUBSET; begin reserve x,y,y1,y2,z,a,b,X,Y,Z,V1,V2 for set, f,g,h,h',f1,f2 for Function, i for Nat, P for Permutation of X, D,D1,D2,D3 for non empty set, d1 for Element of D1, d2 for Element of D2, d3 for Element of D3; theorem :: FUNCT_6:1 x in product <*X*> iff ex y st y in X & x = <*y*>; theorem :: FUNCT_6:2 z in product <*X,Y*> iff ex x,y st x in X & y in Y & z = <*x,y*>; theorem :: FUNCT_6:3 a in product <*X,Y,Z*> iff ex x,y,z st x in X & y in Y & z in Z & a = <*x,y,z*>; theorem :: FUNCT_6:4 product <*D*> = 1-tuples_on D; theorem :: FUNCT_6:5 product <*D1,D2*> = { <*d1,d2*>: not contradiction }; theorem :: FUNCT_6:6 product <*D,D*> = 2-tuples_on D; theorem :: FUNCT_6:7 product <*D1,D2,D3*> = { <*d1,d2,d3*>: not contradiction }; theorem :: FUNCT_6:8 product <*D,D,D*> = 3-tuples_on D; theorem :: FUNCT_6:9 product (i |-> D) = i-tuples_on D; theorem :: FUNCT_6:10 product f c= Funcs(dom f, Union f); begin theorem :: FUNCT_6:11 x in dom ~f implies ex y,z st x = [y,z]; theorem :: FUNCT_6:12 ~([:X,Y:] --> z) = [:Y,X:] --> z; theorem :: FUNCT_6:13 curry f = curry' ~f & uncurry f = ~uncurry' f; theorem :: FUNCT_6:14 [:X,Y:] <> {} implies curry ([:X,Y:] --> z) = X --> (Y --> z) & curry' ([:X,Y:] --> z) = Y --> (X --> z); theorem :: FUNCT_6:15 uncurry (X --> (Y --> z)) = [:X,Y:] --> z & uncurry' (X --> (Y --> z)) = [:Y,X:] --> z; theorem :: FUNCT_6:16 x in dom f & g = f.x implies rng g c= rng uncurry f & rng g c= rng uncurry' f; theorem :: FUNCT_6:17 dom uncurry (X --> f) = [:X,dom f:] & rng uncurry (X --> f) c= rng f & dom uncurry' (X --> f) = [:dom f,X:] & rng uncurry' (X --> f) c= rng f; theorem :: FUNCT_6:18 X <> {} implies rng uncurry (X --> f) = rng f & rng uncurry' (X --> f) = rng f; theorem :: FUNCT_6:19 [:X,Y:] <> {} & f in Funcs([:X,Y:],Z) implies curry f in Funcs(X,Funcs(Y,Z)) & curry' f in Funcs(Y,Funcs(X,Z)); theorem :: FUNCT_6:20 f in Funcs(X,Funcs(Y,Z)) implies uncurry f in Funcs([:X,Y:],Z) & uncurry' f in Funcs([:Y,X:],Z); theorem :: FUNCT_6:21 (curry f in Funcs(X,Funcs(Y,Z)) or curry' f in Funcs(Y,Funcs(X,Z))) & dom f c= [:V1,V2:] implies f in Funcs([:X,Y:],Z); theorem :: FUNCT_6:22 (uncurry f in Funcs([:X,Y:],Z) or uncurry' f in Funcs([:Y,X:],Z)) & rng f c= PFuncs(V1,V2) & dom f = X implies f in Funcs(X,Funcs(Y,Z)); theorem :: FUNCT_6:23 f in PFuncs([:X,Y:],Z) implies curry f in PFuncs(X,PFuncs(Y,Z)) & curry' f in PFuncs(Y,PFuncs(X,Z)); theorem :: FUNCT_6:24 f in PFuncs(X,PFuncs(Y,Z)) implies uncurry f in PFuncs([:X,Y:],Z) & uncurry' f in PFuncs([:Y,X:],Z); theorem :: FUNCT_6:25 (curry f in PFuncs(X,PFuncs(Y,Z)) or curry' f in PFuncs(Y,PFuncs(X,Z))) & dom f c= [:V1,V2:] implies f in PFuncs([:X,Y:],Z); theorem :: FUNCT_6:26 (uncurry f in PFuncs([:X,Y:],Z) or uncurry' f in PFuncs([:Y,X:],Z)) & rng f c= PFuncs(V1,V2) & dom f c= X implies f in PFuncs(X,PFuncs(Y,Z)); begin definition let X be set; func SubFuncs X means :: FUNCT_6:def 1 x in it iff x in X & x is Function; end; theorem :: FUNCT_6:27 SubFuncs X c= X; theorem :: FUNCT_6:28 x in f"SubFuncs rng f iff x in dom f & f.x is Function; theorem :: FUNCT_6:29 SubFuncs {} = {} & SubFuncs {f} = {f} & SubFuncs {f,g} = {f,g} & SubFuncs {f,g,h} = {f,g,h}; theorem :: FUNCT_6:30 Y c= SubFuncs X implies SubFuncs Y = Y; definition let f be Function; func doms f -> Function means :: FUNCT_6:def 2 dom it = f"SubFuncs rng f & for x st x in f"SubFuncs rng f holds it.x = proj1 (f.x); func rngs f -> Function means :: FUNCT_6:def 3 dom it = f"SubFuncs rng f & for x st x in f"SubFuncs rng f holds it.x = proj2 (f.x); func meet f equals :: FUNCT_6:def 4 meet rng f; end; theorem :: FUNCT_6:31 x in dom f & g = f.x implies x in dom doms f & (doms f).x = dom g & x in dom rngs f & (rngs f).x = rng g; theorem :: FUNCT_6:32 doms {} = {} & rngs {} = {}; theorem :: FUNCT_6:33 doms <*f*> = <*dom f*> & rngs <*f*> = <*rng f*>; theorem :: FUNCT_6:34 doms <*f,g*> = <*dom f, dom g*> & rngs <*f,g*> = <*rng f, rng g*>; theorem :: FUNCT_6:35 doms <*f,g,h*> = <*dom f, dom g, dom h*> & rngs <*f,g,h*> = <*rng f, rng g, rng h*>; theorem :: FUNCT_6:36 doms (X --> f) = X --> dom f & rngs (X --> f) = X --> rng f; theorem :: FUNCT_6:37 f <> {} implies (x in meet f iff for y st y in dom f holds x in f.y); theorem :: FUNCT_6:38 meet {} = {}; theorem :: FUNCT_6:39 Union <*X*> = X & meet <*X*> = X; theorem :: FUNCT_6:40 Union <*X,Y*> = X \/ Y & meet <*X,Y*> = X /\ Y; theorem :: FUNCT_6:41 Union <*X,Y,Z*> = X \/ Y \/ Z & meet <*X,Y,Z*> = X /\ Y /\ Z; theorem :: FUNCT_6:42 Union ({} --> Y) = {} & meet ({} --> Y) = {}; theorem :: FUNCT_6:43 X <> {} implies Union (X --> Y) = Y & meet (X --> Y) = Y; definition let f be Function, x, y be set; func f..(x,y) -> set equals :: FUNCT_6:def 5 (uncurry f).[x,y]; end; theorem :: FUNCT_6:44 x in dom f & g = f.x & y in dom g implies f..(x,y) = g.y; theorem :: FUNCT_6:45 x in dom f implies <*f*>..(1,x) = f.x & <*f,g*>..(1,x) = f.x & <*f,g,h*>..(1,x) = f.x; theorem :: FUNCT_6:46 x in dom g implies <*f,g*>..(2,x) = g.x & <*f,g,h*>..(2,x) = g.x; theorem :: FUNCT_6:47 x in dom h implies <*f,g,h*>..(3,x) = h.x; theorem :: FUNCT_6:48 x in X & y in dom f implies (X --> f)..(x,y) = f.y; begin definition let f be Function; func <:f:> -> Function equals :: FUNCT_6:def 6 curry ((uncurry' f)|[:meet doms f, dom f:]); end; theorem :: FUNCT_6:49 dom <:f:> = meet doms f & rng <:f:> c= product rngs f; theorem :: FUNCT_6:50 x in dom <:f:> implies <:f:>.x is Function; theorem :: FUNCT_6:51 x in dom <:f:> & g = <:f:>.x implies dom g = f"SubFuncs rng f & for y st y in dom g holds [y,x] in dom uncurry f & g.y = (uncurry f).[y,x]; theorem :: FUNCT_6:52 x in dom <:f:> implies for g st g in rng f holds x in dom g; theorem :: FUNCT_6:53 g in rng f & (for g st g in rng f holds x in dom g) implies x in dom <:f:>; theorem :: FUNCT_6:54 x in dom f & g = f.x & y in dom <:f:> & h = <:f:>.y implies g.y = h.x; theorem :: FUNCT_6:55 x in dom f & f.x is Function & y in dom <:f:> implies f..(x,y) = <:f:>..(y,x ); definition let f be Function; func Frege f -> Function means :: FUNCT_6:def 7 dom it = product doms f & for g st g in product doms f ex h st it.g = h & dom h = f"SubFuncs rng f & for x st x in dom h holds h.x = (uncurry f).[x,g.x]; end; theorem :: FUNCT_6:56 g in product doms f & x in dom g implies (Frege f)..(g,x) = f..(x,g.x); theorem :: FUNCT_6:57 x in dom f & g = f.x & h in product doms f & h' = (Frege f).h implies h.x in dom g & h'.x = g.(h.x) & h' in product rngs f; theorem :: FUNCT_6:58 rng Frege f = product rngs f; theorem :: FUNCT_6:59 not {} in rng f implies (Frege f is one-to-one iff for g st g in rng f holds g is one-to-one); begin theorem :: FUNCT_6:60 <:{}:> = {} & Frege{} = {{}} --> {}; theorem :: FUNCT_6:61 dom <:<*h*>:> = dom h & for x st x in dom h holds <:<*h*>:>.x = <*h.x*>; theorem :: FUNCT_6:62 dom <:<*f1,f2*>:> = dom f1 /\ dom f2 & for x st x in dom f1 /\ dom f2 holds <:<*f1,f2*>:>.x = <*f1.x,f2.x*>; theorem :: FUNCT_6:63 X <> {} implies dom <:X --> f:> = dom f & for x st x in dom f holds <:X --> f:>.x = X --> f.x; theorem :: FUNCT_6:64 dom Frege<*h*> = product <*dom h*> & rng Frege<*h*> = product <*rng h*> & for x st x in dom h holds (Frege<*h*>).<*x*> = <*h.x*>; theorem :: FUNCT_6:65 dom Frege<*f1,f2*> = product <*dom f1, dom f2*> & rng Frege<*f1,f2*> = product <*rng f1, rng f2*> & for x,y st x in dom f1 & y in dom f2 holds (Frege<*f1,f2*>).<*x,y*> = <*f1.x, f2.y*>; theorem :: FUNCT_6:66 dom Frege(X-->f) = Funcs(X,dom f) & rng Frege(X-->f) = Funcs(X,rng f) & for g st g in Funcs(X,dom f) holds (Frege(X-->f)).g = f*g; theorem :: FUNCT_6:67 x in dom f1 & x in dom f2 implies for y1,y2 holds <:f1,f2:>.x = [y1,y2] iff <:<*f1,f2*>:>.x = <*y1,y2*>; theorem :: FUNCT_6:68 x in dom f1 & y in dom f2 implies for y1,y2 holds [:f1,f2:].[x,y] = [y1,y2] iff (Frege<*f1,f2*>).<*x,y*> = <*y1,y2*>; theorem :: FUNCT_6:69 dom f = X & dom g = X & (for x st x in X holds f.x,g.x are_equipotent) implies product f,product g are_equipotent; theorem :: FUNCT_6:70 dom f = dom h & dom g = rng h & h is one-to-one & (for x st x in dom h holds f.x, g.(h.x) are_equipotent) implies product f,product g are_equipotent; theorem :: FUNCT_6:71 dom f = X implies product f,product (f*P) are_equipotent; begin definition let f,X; func Funcs(f,X) -> Function means :: FUNCT_6:def 8 dom it = dom f & for x st x in dom f holds it.x = Funcs(f.x,X); end; theorem :: FUNCT_6:72 not {} in rng f implies Funcs(f,{}) = dom f --> {}; theorem :: FUNCT_6:73 Funcs({},X) = {}; theorem :: FUNCT_6:74 Funcs(<*X*>,Y) = <*Funcs(X,Y)*>; theorem :: FUNCT_6:75 Funcs(<*X,Y*>,Z) = <*Funcs(X,Z), Funcs(Y,Z)*>; theorem :: FUNCT_6:76 Funcs(X --> Y, Z) = X --> Funcs(Y,Z); theorem :: FUNCT_6:77 Funcs(Union disjoin f,X),product Funcs(f,X) are_equipotent; definition let X,f; func Funcs(X,f) -> Function means :: FUNCT_6:def 9 dom it = dom f & for x st x in dom f holds it.x = Funcs(X,f.x); end; theorem :: FUNCT_6:78 Funcs({},f) = dom f --> {{}}; theorem :: FUNCT_6:79 Funcs(X,{}) = {}; theorem :: FUNCT_6:80 Funcs(X,<*Y*>) = <*Funcs(X,Y)*>; theorem :: FUNCT_6:81 Funcs(X,<*Y,Z*>) = <*Funcs(X,Y), Funcs(X,Z)*>; theorem :: FUNCT_6:82 Funcs(X, Y --> Z) = Y --> Funcs(X,Z); theorem :: FUNCT_6:83 product Funcs(X,f),Funcs(X, product f) are_equipotent;

Back to top