:: 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;