The abstract of the Mizar article:

Curried and Uncurried Functions

by

Grzegorz Bancerek

Received March 6, 1990

MML identifier: FUNCT_5

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, BOOLE, MCART_1, TARSKI, FUNCT_2, PARTFUN1,
      CARD_1, FUNCOP_1, FUNCT_4, FUNCT_3, FUNCT_5;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, WELLORD2,
      FUNCT_2, MCART_1, FUNCT_3, CARD_1, PARTFUN1, FUNCOP_1, FUNCT_4;
 constructors WELLORD2, MCART_1, FUNCT_3, CARD_1, PARTFUN1, FUNCOP_1, FUNCT_4,
      XBOOLE_0;
 clusters RELAT_1, FUNCT_1, FUNCOP_1, RELSET_1, SUBSET_1, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

 reserve X,Y,Z,X1,X2,Y1,Y2,x,y,z,t,x1,x2 for set,
         f,g,h,f1,f2,g1,g2 for Function;

scheme LambdaFS { FS()->set, f(set)->set }:
 ex f st dom f = FS() & for g st g in FS() holds f.g = f(g);

theorem :: FUNCT_5:1
  ~{} = {};

 definition let X;
  func proj1 X -> set means
:: FUNCT_5:def 1
   x in it iff ex y st [x,y] in X;
  func proj2 X -> set means
:: FUNCT_5:def 2
   y in it iff ex x st [x,y] in X;
 end;

canceled 2;

theorem :: FUNCT_5:4
   [x,y] in X implies x in proj1 X & y in proj2 X;

theorem :: FUNCT_5:5
  X c= Y implies proj1 X c= proj1 Y & proj2 X c= proj2 Y;

theorem :: FUNCT_5:6
  proj1(X \/ Y) = proj1 X \/ proj1 Y & proj2(X \/ Y) = proj2 X \/ proj2 Y;

theorem :: FUNCT_5:7
    proj1(X /\ Y) c= proj1 X /\ proj1 Y & proj2(X /\ Y) c= proj2 X /\ proj2 Y;

theorem :: FUNCT_5:8
  proj1 X \ proj1 Y c= proj1(X \ Y) & proj2 X \ proj2 Y c= proj2(X \ Y);

theorem :: FUNCT_5:9
   proj1 X \+\ proj1 Y c= proj1(X \+\ Y) & proj2 X \+\ proj2 Y c= proj2(X \+\ Y
);

theorem :: FUNCT_5:10
  proj1 {} = {} & proj2 {} = {};

theorem :: FUNCT_5:11
  Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} implies
   proj1 [:X,Y:] = X & proj2 [:Y,X:] = X;

theorem :: FUNCT_5:12
  proj1 [:X,Y:] c= X & proj2 [:X,Y:] c= Y;

theorem :: FUNCT_5:13
  Z c= [:X,Y:] implies proj1 Z c= X & proj2 Z c= Y;

canceled;

theorem :: FUNCT_5:15
  proj1 {[x,y]} = {x} & proj2 {[x,y]} = {y};

theorem :: FUNCT_5:16
   proj1 {[x,y],[z,t]} = {x,z} & proj2 {[x,y],[z,t]} = {y,t};

theorem :: FUNCT_5:17
  not (ex x,y st [x,y] in X) implies proj1 X = {} & proj2 X = {};

theorem :: FUNCT_5:18
    proj1 X = {} or proj2 X = {}
 implies not ex x,y st [x,y] in X;

theorem :: FUNCT_5:19
   proj1 X = {} iff proj2 X = {};

theorem :: FUNCT_5:20
  proj1 dom f = proj2 dom ~f & proj2 dom f = proj1 dom ~f;

theorem :: FUNCT_5:21
   for f being Relation holds
  proj1 f = dom f & proj2 f = rng f;

 definition let f;
  func curry f -> Function means
:: FUNCT_5:def 3
   dom it = proj1 dom f & for x st x in proj1 dom f ex g st it.x = g &
   dom g = proj2 (dom f /\ [:{x},proj2 dom f:]) &
    for y st y in dom g holds g.y = f.[x,y];
  func uncurry f -> Function means
:: FUNCT_5:def 4
   (for t holds t in dom it iff
    ex x,g,y st t = [x,y] & x in dom f & g = f.x & y in dom g) &
     for x,g st x in dom it & g = f.x`1 holds it.x = g.x`2;
 end;

 definition let f;
  func curry' f -> Function equals
:: FUNCT_5:def 5
    curry ~f;
  func uncurry' f -> Function equals
:: FUNCT_5:def 6
    ~(uncurry f);
 end;

canceled 4;

theorem :: FUNCT_5:26
  [x,y] in dom f implies x in dom curry f & (curry f).x is Function;

theorem :: FUNCT_5:27
  [x,y] in dom f & g = (curry f).x implies y in dom g & g.y = f.[x,y];

theorem :: FUNCT_5:28
    [x,y] in dom f implies y in dom curry' f & (curry' f).y is Function;

theorem :: FUNCT_5:29
    [x,y] in dom f & g = (curry' f).y implies x in dom g & g.x = f.[x,y];

theorem :: FUNCT_5:30
   dom curry' f = proj2 dom f;

theorem :: FUNCT_5:31
 [:X,Y:] <> {} & dom f = [:X,Y:] implies dom curry f = X & dom curry' f = Y;

theorem :: FUNCT_5:32
  dom f c= [:X,Y:] implies dom curry f c= X & dom curry' f c= Y;

theorem :: FUNCT_5:33
  rng f c= Funcs(X,Y) implies
   dom uncurry f = [:dom f,X:] & dom uncurry' f = [:X,dom f:];

theorem :: FUNCT_5:34
   not (ex x,y st [x,y] in dom f) implies curry f = {} & curry' f = {};

theorem :: FUNCT_5:35
   not (ex x st x in dom f & f.x is Function) implies
   uncurry f = {} & uncurry' f = {};

theorem :: FUNCT_5:36
  [:X,Y:] <> {} & dom f = [:X,Y:] & x in X implies
  ex g st (curry f).x = g & dom g = Y & rng g c= rng f &
   for y st y in Y holds g.y = f.[x,y];

theorem :: FUNCT_5:37
  x in dom curry f implies (curry f).x is Function;

theorem :: FUNCT_5:38
  x in dom curry f & g = (curry f).x implies
  dom g = proj2 (dom f /\ [:{x},proj2 dom f:]) & dom g c= proj2 dom f &
   rng g c= rng f & for y st y in dom g holds g.y = f.[x,y] & [x,y] in dom f;

theorem :: FUNCT_5:39
  [:X,Y:] <> {} & dom f = [:X,Y:] & y in Y implies
  ex g st (curry' f).y = g & dom g = X & rng g c= rng f &
   for x st x in X holds g.x = f.[x,y];

theorem :: FUNCT_5:40
    x in dom curry' f implies (curry' f).x is Function;

theorem :: FUNCT_5:41
    x in dom curry' f & g = (curry' f).x implies
  dom g = proj1 (dom f /\ [:proj1 dom f,{x}:]) & dom g c= proj1 dom f &
   rng g c= rng f & for y st y in dom g holds g.y = f.[y,x] & [y,x] in dom f;

theorem :: FUNCT_5:42
  dom f = [:X,Y:] implies
   rng curry f c= Funcs(Y,rng f) & rng curry' f c= Funcs(X,rng f);

theorem :: FUNCT_5:43
   rng curry f c= PFuncs(proj2 dom f,rng f) &
   rng curry' f c= PFuncs(proj1 dom f,rng f);

theorem :: FUNCT_5:44
  rng f c= PFuncs(X,Y) implies
   dom uncurry f c= [:dom f,X:] & dom uncurry' f c= [:X,dom f:];

theorem :: FUNCT_5:45
  x in dom f & g = f.x & y in dom g implies
   [x,y] in dom uncurry f & (uncurry f).[x,y] = g.y & g.y in rng uncurry f;

theorem :: FUNCT_5:46
    x in dom f & g = f.x & y in dom g implies
   [y,x] in dom uncurry' f & (uncurry' f).[y,x] = g.y & g.y in rng uncurry' f;

theorem :: FUNCT_5:47
  rng f c= PFuncs(X,Y) implies rng uncurry f c= Y & rng uncurry' f c= Y;

theorem :: FUNCT_5:48
  rng f c= Funcs(X,Y) implies rng uncurry f c= Y & rng uncurry' f c= Y;

theorem :: FUNCT_5:49
  curry {} = {} & curry' {} = {};

theorem :: FUNCT_5:50
  uncurry {} = {} & uncurry' {} = {};

theorem :: FUNCT_5:51
 dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry f1 = curry f2 implies f1 = f2;

theorem :: FUNCT_5:52
 dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry' f1 = curry' f2 implies f1 = f2;

theorem :: FUNCT_5:53
  rng f1 c= Funcs(X,Y) & rng f2 c= Funcs(X,Y) & X <> {} &
   uncurry f1 = uncurry f2 implies f1 = f2;

theorem :: FUNCT_5:54
   rng f1 c= Funcs(X,Y) & rng f2 c= Funcs(X,Y) & X <> {} &
   uncurry' f1 = uncurry' f2 implies f1 = f2;

theorem :: FUNCT_5:55
  rng f c= Funcs(X,Y) & X <> {} implies
   curry uncurry f = f & curry' uncurry' f = f;

theorem :: FUNCT_5:56
   dom f = [:X,Y:] implies uncurry curry f = f & uncurry' curry' f = f;

theorem :: FUNCT_5:57
  dom f c= [:X,Y:] implies uncurry curry f = f & uncurry' curry' f = f;

theorem :: FUNCT_5:58
  rng f c= PFuncs(X,Y) & not {} in rng f implies
   curry uncurry f = f & curry' uncurry' f = f;

theorem :: FUNCT_5:59
   dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry f1 = curry f2 implies f1 = f2;

theorem :: FUNCT_5:60
   dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry' f1 = curry' f2 implies f1 =
f2;

theorem :: FUNCT_5:61
   rng f1 c= PFuncs(X,Y) & rng f2 c= PFuncs(X,Y) & not {} in rng f1 &
   not {} in rng f2 & uncurry f1 = uncurry f2 implies f1 = f2;

theorem :: FUNCT_5:62
   rng f1 c= PFuncs(X,Y) & rng f2 c= PFuncs(X,Y) & not {} in rng f1 &
   not {} in rng f2 & uncurry' f1 = uncurry' f2 implies f1 = f2;

theorem :: FUNCT_5:63
  X c= Y implies Funcs(Z,X) c= Funcs(Z,Y);

theorem :: FUNCT_5:64
  Funcs({},X) = {{}};

theorem :: FUNCT_5:65
    X,Funcs({x},X) are_equipotent & Card X = Card Funcs({x},X);

theorem :: FUNCT_5:66
  Funcs(X,{x}) = {X --> x};

theorem :: FUNCT_5:67
  X1,Y1 are_equipotent & X2,Y2 are_equipotent implies
   Funcs(X1,X2),Funcs(Y1,Y2) are_equipotent &
   Card Funcs(X1,X2) = Card Funcs(Y1,Y2);

theorem :: FUNCT_5:68
    Card X1 = Card Y1 & Card X2 = Card Y2 implies
   Card Funcs(X1,X2) = Card Funcs(Y1,Y2);

theorem :: FUNCT_5:69
    X1 misses X2 implies
  Funcs(X1 \/ X2,X),[:Funcs(X1,X),Funcs(X2,X):] are_equipotent &
   Card Funcs(X1 \/ X2,X) = Card [:Funcs(X1,X),Funcs(X2,X):];

theorem :: FUNCT_5:70
    Funcs([:X,Y:],Z),Funcs(X,Funcs(Y,Z)) are_equipotent &
   Card Funcs([:X,Y:],Z) = Card Funcs(X,Funcs(Y,Z));

theorem :: FUNCT_5:71
   Funcs(Z,[:X,Y:]),[:Funcs(Z,X),Funcs(Z,Y):] are_equipotent &
   Card Funcs(Z,[:X,Y:]) = Card [:Funcs(Z,X),Funcs(Z,Y):];

theorem :: FUNCT_5:72
   x <> y implies Funcs(X,{x,y}),bool X are_equipotent &
 Card Funcs(X,{x,y}) = Card bool X;

theorem :: FUNCT_5:73
   x <> y implies Funcs({x,y},X),[:X,X:] are_equipotent &
   Card Funcs({x,y},X) = Card [:X,X:];