:: Cartesian Product of Functions :: by Grzegorz Bancerek :: :: Received September 30, 1991 :: Copyright (c) 1991-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies FUNCT_1, SUBSET_1, FUNCT_2, XBOOLE_0, CARD_3, RELAT_1, FUNCOP_1, TARSKI, ZFMISC_1, FUNCT_5, PARTFUN1, SETFAM_1, FINSEQ_4, MCART_1, FUNCT_6, NAT_1; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, XTUPLE_0, MCART_1, SETFAM_1, FUNCT_2, BINOP_1, PARTFUN1, FUNCT_3, WELLORD2, FUNCOP_1, FUNCT_4, FUNCT_5, ORDINAL1, CARD_3; constructors ENUMSET1, SETFAM_1, PARTFUN1, WELLORD2, BINOP_1, FUNCT_3, FUNCOP_1, FUNCT_4, FUNCT_5, CARD_3, RELSET_1, FINSET_1, DOMAIN_1, XTUPLE_0; registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, RELSET_1, XTUPLE_0, FUNCT_5, CARD_3; requirements BOOLE, SUBSET; begin reserve x,y,y1,y2,z,a,b for object, X,Y,Z,V1,V2 for set, f,g,h,h9,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 product f c= Funcs(dom f, Union f); begin theorem :: FUNCT_6:2 x in dom ~f implies ex y,z being object st x = [y,z]; theorem :: FUNCT_6:3 ~([:X,Y:] --> z) = [:Y,X:] --> z; theorem :: FUNCT_6:4 curry f = curry' ~f & uncurry f = ~uncurry' f; theorem :: FUNCT_6:5 [:X,Y:] <> {} implies curry ([:X,Y:] --> z) = X --> (Y --> z) & curry' ([:X,Y:] --> z) = Y --> (X --> z); theorem :: FUNCT_6:6 uncurry (X --> (Y --> z)) = [:X,Y:] --> z & uncurry' (X --> (Y --> z)) = [:Y,X:] --> z; theorem :: FUNCT_6:7 x in dom f & g = f.x implies rng g c= rng uncurry f & rng g c= rng uncurry' f ; theorem :: FUNCT_6:8 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:9 X <> {} implies rng uncurry (X --> f) = rng f & rng uncurry' (X --> f) = rng f; theorem :: FUNCT_6:10 [: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:11 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:12 (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:13 (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:14 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:15 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:16 (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:17 (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 ::$CD end; ::$CT 4 definition let f be Function-yielding Function; func doms f -> Function means :: FUNCT_6:def 2 dom it = dom f & for x being object st x in dom f holds it.x = proj1 (f.x); func rngs f -> Function means :: FUNCT_6:def 3 dom it = dom f & for x being object st x in dom f holds it.x = proj2 (f.x); end; definition let f be Function; func meet f -> set equals :: FUNCT_6:def 4 meet rng f; end; theorem :: FUNCT_6:22 for f being Function-yielding Function holds 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:23 doms {} = {} & rngs {} = {}; theorem :: FUNCT_6:24 doms (X --> f) = X --> dom f & rngs (X --> f) = X --> rng f; theorem :: FUNCT_6:25 f <> {} implies for x being object holds x in meet f iff for y being object st y in dom f holds x in f.y; theorem :: FUNCT_6:26 Union ({} --> Y) = {} & meet ({} --> Y) = {}; theorem :: FUNCT_6:27 X <> {} implies Union (X --> Y) = Y & meet (X --> Y) = Y; definition let f be Function, x, y be object; func f..(x,y) -> set equals :: FUNCT_6:def 5 (uncurry f).(x,y); end; theorem :: FUNCT_6:28 x in X & y in dom f implies (X --> f)..(x,y) = f.y; begin definition let f be Function-yielding Function; func <:f:> -> Function equals :: FUNCT_6:def 6 curry ((uncurry' f)|([:meet doms f, dom f:] qua set)); end; theorem :: FUNCT_6:29 for f being Function-yielding Function holds dom <:f:> = meet doms f & rng <:f:> c= product rngs f; registration let f be Function-yielding Function; cluster <:f:> ->Function-yielding; end; ::$CT theorem :: FUNCT_6:31 for f being Function-yielding Function holds x in dom <:f:> & g = <:f:>.x implies dom g = dom f & for y st y in dom g holds [y,x] in dom uncurry f & g.y = (uncurry f).(y,x); theorem :: FUNCT_6:32 for f being Function-yielding Function st x in dom <:f:> for g st g in rng f holds x in dom g; theorem :: FUNCT_6:33 for x being object, f being Function-yielding Function st g in rng f & for g st g in rng f holds x in dom g holds x in dom <:f :>; theorem :: FUNCT_6:34 for f being Function-yielding Function st x in dom f & g = f.x & y in dom <:f:> & h = <:f:>.y holds g.y = h.x; theorem :: FUNCT_6:35 for f being Function-yielding Function st x in dom f & f.x is Function & y in dom <:f:> holds f..(x,y) = <:f:>..( y, x ); definition let f be Function-yielding 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 = dom f & for x st x in dom h holds h.x = (uncurry f).(x,g.x); end; theorem :: FUNCT_6:36 for f being Function-yielding Function st g in product doms f & x in dom g holds (Frege f)..(g,x) = f..(x,g.x); theorem :: FUNCT_6:37 for f being Function-yielding Function st x in dom f & g = f.x & h in product doms f & h9 = (Frege f).h holds h.x in dom g & h9.x = g.(h.x) & h9 in product rngs f; theorem :: FUNCT_6:38 for f being Function-yielding Function holds rng Frege f = product rngs f; theorem :: FUNCT_6:39 for f being Function-yielding Function st not {} in rng f holds (Frege f is one-to-one iff for g st g in rng f holds g is one-to-one); begin theorem :: FUNCT_6:40 <:{}:> = {} & Frege{} = {} .--> {}; theorem :: FUNCT_6:41 X <> {} implies dom <:X --> f:> = dom f & for x st x in dom f holds <: X --> f:>.x = X --> f.x; theorem :: FUNCT_6:42 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:43 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:44 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:45 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 being object st x in dom f holds it.x = Funcs(f.x,X); end; theorem :: FUNCT_6:46 not {} in rng f implies Funcs(f,{}) = dom f --> {}; theorem :: FUNCT_6:47 Funcs({},X) = {}; theorem :: FUNCT_6:48 Funcs(X --> Y, Z) = X --> Funcs(Y,Z); theorem :: FUNCT_6:49 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 being object st x in dom f holds it.x = Funcs(X,f.x); end; theorem :: FUNCT_6:50 Funcs({},f) = dom f --> {{}}; theorem :: FUNCT_6:51 Funcs(X,{}) = {}; theorem :: FUNCT_6:52 Funcs(X, Y --> Z) = Y --> Funcs(X,Z); theorem :: FUNCT_6:53 product Funcs(X,f),Funcs(X, product f) are_equipotent; begin :: Addenda :: from PRALG_2 definition let f be Function; func commute f -> Function-yielding Function equals :: FUNCT_6:def 10 curry' uncurry f; end; theorem :: FUNCT_6:54 for f be Function, x be set st x in dom (commute f) holds (commute f). x is Function; theorem :: FUNCT_6:55 for A,B,C be set, f be Function st A <> {} & B <> {} & f in Funcs(A,Funcs(B,C)) holds commute f in Funcs(B,Funcs(A,C)); theorem :: FUNCT_6:56 for A,B,C be set, f be Function st A <> {} & B <> {} & f in Funcs(A, Funcs(B,C)) for g,h be Function, x,y be set st x in A & y in B & f.x = g & ( commute f).y = h holds h.x = g.y & dom h = A & dom g = B & rng h c= C & rng g c= C; theorem :: FUNCT_6:57 for A,B,C be set, f be Function st A <> {} & B <> {} & f in Funcs(A, Funcs(B,C)) holds commute commute f = f; theorem :: FUNCT_6:58 commute {} = {}; :: from EXTENS_1 theorem :: FUNCT_6:59 for f be Function-yielding Function holds dom doms f = dom f; theorem :: FUNCT_6:60 for f be Function-yielding Function holds dom rngs f = dom f;