The Mizar abstract of FUNCT

Journal of Formalized Mathematics
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;
The abstract of the Mizar article:

Cartesian Product of Functions
