:: Curried and Uncurried Functions
:: by Grzegorz Bancerek
::
:: Copyright (c) 1990-2021 Association of Mizar Users

scheme :: FUNCT_5:sch 1
LambdaFS{ F1() -> set , F2( object ) -> object } :
ex f being Function st
( dom f = F1() & ( for g being Function st g in F1() holds
f . g = F2(g) ) )
proof end;

theorem Th1: :: FUNCT_5:1
proof end;

theorem :: FUNCT_5:2
canceled;

theorem :: FUNCT_5:3
canceled;

theorem :: FUNCT_5:4
canceled;

theorem :: FUNCT_5:5
canceled;

theorem :: FUNCT_5:6
canceled;

theorem :: FUNCT_5:7
canceled;

::$CT 6 theorem Th2: :: FUNCT_5:8 ( proj1 {} = {} & proj2 {} = {} ) ; theorem Th3: :: FUNCT_5:9 for X, Y being set st ( Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} ) holds ( proj1 [:X,Y:] = X & proj2 [:Y,X:] = X ) proof end; theorem Th4: :: FUNCT_5:10 for X, Y being set holds ( proj1 [:X,Y:] c= X & proj2 [:X,Y:] c= Y ) proof end; theorem Th5: :: FUNCT_5:11 for X, Y, Z being set st Z c= [:X,Y:] holds ( proj1 Z c= X & proj2 Z c= Y ) proof end; theorem Th6: :: FUNCT_5:12 for x, y being object holds ( proj1 {[x,y]} = {x} & proj2 {[x,y]} = {y} ) proof end; theorem :: FUNCT_5:13 for x, y, z, t being object holds ( proj1 {[x,y],[z,t]} = {x,z} & proj2 {[x,y],[z,t]} = {y,t} ) proof end; theorem Th8: :: FUNCT_5:14 for X being set st ( for x, y being object holds not [x,y] in X ) holds ( proj1 X = {} & proj2 X = {} ) proof end; theorem :: FUNCT_5:15 for X being set st ( proj1 X = {} or proj2 X = {} ) holds for x, y being object holds not [x,y] in X by ; theorem :: FUNCT_5:16 for X being set holds ( proj1 X = {} iff proj2 X = {} ) proof end; theorem Th11: :: FUNCT_5:17 for f being Function holds ( proj1 (dom f) = proj2 (dom (~ f)) & proj2 (dom f) = proj1 (dom (~ f)) ) proof end; definition let f be Function; func curry f -> Function means :Def1: :: FUNCT_5:def 1 ( dom it = proj1 (dom f) & ( for x being object st x in proj1 (dom f) holds ex g being Function st ( it . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object st y in dom g holds g . y = f . (x,y) ) ) ) ); existence ex b1 being Function st ( dom b1 = proj1 (dom f) & ( for x being object st x in proj1 (dom f) holds ex g being Function st ( b1 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object st y in dom g holds g . y = f . (x,y) ) ) ) ) proof end; uniqueness for b1, b2 being Function st dom b1 = proj1 (dom f) & ( for x being object st x in proj1 (dom f) holds ex g being Function st ( b1 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object st y in dom g holds g . y = f . (x,y) ) ) ) & dom b2 = proj1 (dom f) & ( for x being object st x in proj1 (dom f) holds ex g being Function st ( b2 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object st y in dom g holds g . y = f . (x,y) ) ) ) holds b1 = b2 proof end; func uncurry f -> Function means :Def2: :: FUNCT_5:def 2 ( ( for t being object holds ( t in dom it iff ex x being object ex g being Function ex y being object st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being object for g being Function st x in dom it & g = f . (x 1) holds it . x = g . (x 2) ) ); existence ex b1 being Function st ( ( for t being object holds ( t in dom b1 iff ex x being object ex g being Function ex y being object st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being object for g being Function st x in dom b1 & g = f . (x 1) holds b1 . x = g . (x 2) ) ) proof end; uniqueness for b1, b2 being Function st ( for t being object holds ( t in dom b1 iff ex x being object ex g being Function ex y being object st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being object for g being Function st x in dom b1 & g = f . (x 1) holds b1 . x = g . (x 2) ) & ( for t being object holds ( t in dom b2 iff ex x being object ex g being Function ex y being object st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being object for g being Function st x in dom b2 & g = f . (x 1) holds b2 . x = g . (x 2) ) holds b1 = b2 proof end; end; :: deftheorem Def1 defines curry FUNCT_5:def 1 : for f, b2 being Function holds ( b2 = curry f iff ( dom b2 = proj1 (dom f) & ( for x being object st x in proj1 (dom f) holds ex g being Function st ( b2 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object st y in dom g holds g . y = f . (x,y) ) ) ) ) ); :: deftheorem Def2 defines uncurry FUNCT_5:def 2 : for f, b2 being Function holds ( b2 = uncurry f iff ( ( for t being object holds ( t in dom b2 iff ex x being object ex g being Function ex y being object st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being object for g being Function st x in dom b2 & g = f . (x 1) holds b2 . x = g . (x 2) ) ) ); definition let f be Function; func curry' f -> Function equals :: FUNCT_5:def 3 curry (~ f); correctness coherence curry (~ f) is Function ; ; func uncurry' f -> Function equals :: FUNCT_5:def 4 ~ (); correctness coherence ~ () is Function ; ; end; :: deftheorem defines curry' FUNCT_5:def 3 : for f being Function holds curry' f = curry (~ f); :: deftheorem defines uncurry' FUNCT_5:def 4 : for f being Function holds uncurry' f = ~ (); theorem :: FUNCT_5:18 canceled; ::$CT
registration
let f be Function;
coherence
proof end;
end;

theorem Th12: :: FUNCT_5:19
for f being Function
for x, y being object st [x,y] in dom f holds
x in dom ()
proof end;

theorem Th13: :: FUNCT_5:20
for f, g being Function
for x, y being object st [x,y] in dom f & g = () . x holds
( y in dom g & g . y = f . (x,y) )
proof end;

registration
let f be Function;
coherence ;
end;

theorem :: FUNCT_5:21
for f being Function
for x, y being object st [x,y] in dom f holds
y in dom ()
proof end;

theorem Th15: :: FUNCT_5:22
for f, g being Function
for x, y being object st [x,y] in dom f & g = () . y holds
( x in dom g & g . x = f . (x,y) )
proof end;

theorem :: FUNCT_5:23
for f being Function holds dom () = proj2 (dom f)
proof end;

theorem Th17: :: FUNCT_5:24
for X, Y being set
for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] holds
( dom () = X & dom () = Y )
proof end;

theorem Th18: :: FUNCT_5:25
for X, Y being set
for f being Function st dom f c= [:X,Y:] holds
( dom () c= X & dom () c= Y )
proof end;

theorem Th19: :: FUNCT_5:26
for X, Y being set
for f being Function st rng f c= Funcs (X,Y) holds
( dom () = [:(dom f),X:] & dom () = [:X,(dom f):] )
proof end;

theorem :: FUNCT_5:27
for f being Function st ( for x, y being object holds not [x,y] in dom f ) holds
( curry f = {} & curry' f = {} )
proof end;

theorem :: FUNCT_5:28
for f being Function st ( for x being object holds
( not x in dom f or not f . x is Function ) ) holds
( uncurry f = {} & uncurry' f = {} )
proof end;

theorem Th22: :: FUNCT_5:29
for X, Y being set
for x being object
for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & x in X holds
ex g being Function st
( () . x = g & dom g = Y & rng g c= rng f & ( for y being object st y in Y holds
g . y = f . (x,y) ) )
proof end;

theorem Th23: :: FUNCT_5:30
for x being object
for f being Function st x in dom () holds
() . x is Function
proof end;

theorem Th24: :: FUNCT_5:31
for x being object
for f, g being Function st x in dom () & g = () . x holds
( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & dom g c= proj2 (dom f) & rng g c= rng f & ( for y being object st y in dom g holds
( g . y = f . (x,y) & [x,y] in dom f ) ) )
proof end;

theorem Th25: :: FUNCT_5:32
for X, Y being set
for y being object
for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & y in Y holds
ex g being Function st
( () . y = g & dom g = X & rng g c= rng f & ( for x being object st x in X holds
g . x = f . (x,y) ) )
proof end;

theorem :: FUNCT_5:33
for x being object
for f being Function st x in dom () holds
() . x is Function by Th23;

theorem :: FUNCT_5:34
for x being object
for f, g being Function st x in dom () & g = () . x holds
( dom g = proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) & dom g c= proj1 (dom f) & rng g c= rng f & ( for y being object st y in dom g holds
( g . y = f . (y,x) & [y,x] in dom f ) ) )
proof end;

theorem Th28: :: FUNCT_5:35
for X, Y being set
for f being Function st dom f = [:X,Y:] holds
( rng () c= Funcs (Y,(rng f)) & rng () c= Funcs (X,(rng f)) )
proof end;

theorem :: FUNCT_5:36
for f being Function holds
( rng () c= PFuncs ((proj2 (dom f)),(rng f)) & rng () c= PFuncs ((proj1 (dom f)),(rng f)) )
proof end;

theorem Th30: :: FUNCT_5:37
for X, Y being set
for f being Function st rng f c= PFuncs (X,Y) holds
( dom () c= [:(dom f),X:] & dom () c= [:X,(dom f):] )
proof end;

theorem Th31: :: FUNCT_5:38
for x, y being object
for f, g being Function st x in dom f & g = f . x & y in dom g holds
( [x,y] in dom () & () . (x,y) = g . y & g . y in rng () )
proof end;

theorem :: FUNCT_5:39
for x, y being object
for f, g being Function st x in dom f & g = f . x & y in dom g holds
( [y,x] in dom () & () . (y,x) = g . y & g . y in rng () )
proof end;

theorem Th33: :: FUNCT_5:40
for X, Y being set
for f being Function st rng f c= PFuncs (X,Y) holds
( rng () c= Y & rng () c= Y )
proof end;

theorem Th34: :: FUNCT_5:41
for X, Y being set
for f being Function st rng f c= Funcs (X,Y) holds
( rng () c= Y & rng () c= Y )
proof end;

theorem Th35: :: FUNCT_5:42
( curry {} = {} & curry' {} = {} ) by ;

theorem Th36: :: FUNCT_5:43
proof end;

theorem Th37: :: FUNCT_5:44
for X, Y being set
for f1, f2 being Function st dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry f1 = curry f2 holds
f1 = f2
proof end;

theorem Th38: :: FUNCT_5:45
for X, Y being set
for f1, f2 being Function st dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry' f1 = curry' f2 holds
f1 = f2
proof end;

theorem Th39: :: FUNCT_5:46
for X, Y being set
for f1, f2 being Function st rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry f1 = uncurry f2 holds
f1 = f2
proof end;

theorem :: FUNCT_5:47
for X, Y being set
for f1, f2 being Function st rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry' f1 = uncurry' f2 holds
f1 = f2
proof end;

theorem Th41: :: FUNCT_5:48
for X, Y being set
for f being Function st rng f c= Funcs (X,Y) & X <> {} holds
( curry () = f & curry' () = f )
proof end;

theorem :: FUNCT_5:49
for X, Y being set
for f being Function st dom f = [:X,Y:] holds
( uncurry () = f & uncurry' () = f )
proof end;

theorem Th43: :: FUNCT_5:50
for X, Y being set
for f being Function st dom f c= [:X,Y:] holds
( uncurry () = f & uncurry' () = f )
proof end;

theorem Th44: :: FUNCT_5:51
for X, Y being set
for f being Function st rng f c= PFuncs (X,Y) & not {} in rng f holds
( curry () = f & curry' () = f )
proof end;

theorem :: FUNCT_5:52
for X, Y being set
for f1, f2 being Function st dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry f1 = curry f2 holds
f1 = f2
proof end;

theorem :: FUNCT_5:53
for X, Y being set
for f1, f2 being Function st dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry' f1 = curry' f2 holds
f1 = f2
proof end;

theorem :: FUNCT_5:54
for X, Y being set
for f1, f2 being Function st rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry f1 = uncurry f2 holds
f1 = f2
proof end;

theorem :: FUNCT_5:55
for X, Y being set
for f1, f2 being Function st rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry' f1 = uncurry' f2 holds
f1 = f2
proof end;

theorem Th49: :: FUNCT_5:56
for X, Y, Z being set st X c= Y holds
Funcs (Z,X) c= Funcs (Z,Y)
proof end;

theorem Th50: :: FUNCT_5:57
for X being set holds Funcs ({},X) =
proof end;

theorem :: FUNCT_5:58
for X being set
for x being object holds
( X, Funcs ({x},X) are_equipotent & card X = card (Funcs ({x},X)) )
proof end;

theorem Th52: :: FUNCT_5:59
for X being set
for x being object holds Funcs (X,{x}) = {(X --> x)}
proof end;

theorem Th53: :: FUNCT_5:60
for X1, X2, Y1, Y2 being set st X1,Y1 are_equipotent & X2,Y2 are_equipotent holds
( Funcs (X1,X2), Funcs (Y1,Y2) are_equipotent & card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) )
proof end;

theorem :: FUNCT_5:61
for X1, X2, Y1, Y2 being set st card X1 = card Y1 & card X2 = card Y2 holds
card (Funcs (X1,X2)) = card (Funcs (Y1,Y2))
proof end;

theorem :: FUNCT_5:62
for X, X1, X2 being set st X1 misses X2 holds
( Funcs ((X1 \/ X2),X),[:(Funcs (X1,X)),(Funcs (X2,X)):] are_equipotent & card (Funcs ((X1 \/ X2),X)) = card [:(Funcs (X1,X)),(Funcs (X2,X)):] )
proof end;

theorem :: FUNCT_5:63
for X, Y, Z being set holds
( Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent & card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) )
proof end;

theorem :: FUNCT_5:64
for X, Y, Z being set holds
( Funcs (Z,[:X,Y:]),[:(Funcs (Z,X)),(Funcs (Z,Y)):] are_equipotent & card (Funcs (Z,[:X,Y:])) = card [:(Funcs (Z,X)),(Funcs (Z,Y)):] )
proof end;

theorem :: FUNCT_5:65
for X being set
for x, y being object st x <> y holds
( Funcs (X,{x,y}), bool X are_equipotent & card (Funcs (X,{x,y})) = card (bool X) )
proof end;

theorem :: FUNCT_5:66
for X being set
for x, y being object st x <> y holds
( Funcs ({x,y},X),[:X,X:] are_equipotent & card (Funcs ({x,y},X)) = card [:X,X:] )
proof end;

notation
synonym op0 for 0 ;
end;

definition
:: original: op0
redefine func op0 -> Element of ;
coherence
op0 is Element of
by TARSKI:def 1;
end;

definition
func op1 -> set equals :: FUNCT_5:def 5
0 .--> 0;
coherence ;
func op2 -> set equals :: FUNCT_5:def 6
(0,0) :-> 0;
coherence
(0,0) :-> 0 is set
;
end;

:: deftheorem defines op1 FUNCT_5:def 5 :

:: deftheorem defines op2 FUNCT_5:def 6 :
op2 = (0,0) :-> 0;

definition
:: original: op1
redefine func op1 -> UnOp of ;
coherence
op1 is UnOp of
;
:: original: op2
redefine func op2 -> BinOp of ;
coherence
op2 is BinOp of
;
end;

definition
let D be non empty set ;
let X be set ;
let E be non empty set ;
let F be FUNCTION_DOMAIN of X,E;
let f be Function of D,F;
let d be Element of D;
:: original: .
redefine func f . d -> Element of F;
coherence
f . d is Element of F
proof end;
end;

theorem Th60: :: FUNCT_5:67
for C, D, E being non empty set
for f being Function of [:C,D:],E holds curry f is Function of C,(Funcs (D,E))
proof end;

theorem Th61: :: FUNCT_5:68
for C, D, E being non empty set
for f being Function of [:C,D:],E holds curry' f is Function of D,(Funcs (C,E))
proof end;

definition
let C, D, E be non empty set ;
let f be Function of [:C,D:],E;
:: original: curry
redefine func curry f -> Function of C,(Funcs (D,E));
coherence
curry f is Function of C,(Funcs (D,E))
by Th60;
:: original: curry'
redefine func curry' f -> Function of D,(Funcs (C,E));
coherence
curry' f is Function of D,(Funcs (C,E))
by Th61;
end;

theorem :: FUNCT_5:69
for C, D, E being non empty set
for c being Element of C
for d being Element of D
for f being Function of [:C,D:],E holds f . (c,d) = (() . c) . d
proof end;

theorem :: FUNCT_5:70
for C, D, E being non empty set
for c being Element of C
for d being Element of D
for f being Function of [:C,D:],E holds f . (c,d) = (() . d) . c
proof end;

:: from ISOCAT_2, 2011.11.25, A.T.
definition
let A, B, C be non empty set ;
let f be Function of A,(Funcs (B,C));
:: original: uncurry
redefine func uncurry f -> Function of [:A,B:],C;
coherence
uncurry f is Function of [:A,B:],C
proof end;
end;

theorem :: FUNCT_5:71
for A, B, C being non empty set
for f being Function of A,(Funcs (B,C)) holds curry () = f
proof end;

theorem :: FUNCT_5:72
for A, B, C being non empty set
for f being Function of A,(Funcs (B,C))
for a being Element of A
for b being Element of B holds () . (a,b) = (f . a) . b
proof end;