:: Partial Functions
:: by Czes{\l}aw Byli\'nski
::
:: Received September 18, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

:: Auxiliary theorems
theorem Th1: :: PARTFUN1:1
for f, g being Function st ( for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x ) holds
ex h being Function st f \/ g = h
proofend;

theorem Th2: :: PARTFUN1:2
for f, g, h being Function st f \/ g = h holds
for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x
proofend;

scheme :: PARTFUN1:sch 1
LambdaC{ F1() ->  set , P1[ set ], F2( set ) ->  set , F3( set ) ->  set } :
 ex f being Function st
( dom f = F1() & ( for x being set st x in F1() holds
( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) )
proofend;

Lm1: now__::_thesis:_for_X,_Y_being_set_ex_E_being_set_st_
(_dom_E_c=_X_&_rng_E_c=_Y_)
let X, Y be set ; ::_thesis: ex E being set st
( dom E c= X & rng E c= Y )
take E = {} ; ::_thesis: ( dom E c= X & rng E c= Y )
thus  ( dom E c= X & rng E c= Y ) by XBOOLE_1:2; ::_thesis: verum
end;

registration
let X, Y be set ;
cluster Relation-like X -defined Y -valued Function-like for Element of bool [:X,Y:];
existence
 ex b1 being Relation of X,Y st b1 is Function-like
proofend;
end;

definition
let X, Y be set ;
mode PartFunc of X,Y is Function-like Relation of X,Y;
end;

theorem :: PARTFUN1:3
for X, Y, y being set
for f being PartFunc of X,Y st y in rng f holds
ex x being Element of X st
( x in dom f & y = f . x )
proofend;

theorem Th4: :: PARTFUN1:4
for Y, x being set
for f being b1 -valued Function st x in dom f holds
f . x in Y
proofend;

theorem :: PARTFUN1:5
for X, Y being set
for f1, f2 being PartFunc of X,Y st dom f1 = dom f2 & ( for x being Element of X st x in dom f1 holds
f1 . x = f2 . x ) holds
f1 = f2
proofend;

scheme :: PARTFUN1:sch 2
PartFuncEx{ F1() ->  set , F2() ->  set , P1[ set , set ] } :
 ex f being PartFunc of F1(),F2() st
( ( for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds
P1[x,f . x] ) )
provided
A1: for x, y being set st x in F1() & P1[x,y] holds
y in F2() and
A2: for x, y1, y2 being set st x in F1() & P1[x,y1] & P1[x,y2] holds
y1 = y2
proofend;

scheme :: PARTFUN1:sch 3
LambdaR{ F1() ->  set , F2() ->  set , F3( set ) ->  set , P1[ set ] } :
 ex f being PartFunc of F1(),F2() st
( ( for x being set holds
( x in dom f iff ( x in F1() & P1[x] ) ) ) & ( for x being set st x in dom f holds
f . x = F3(x) ) )
provided
A1: for x being set st P1[x] holds
F3(x) in F2()
proofend;

definition
let X, Y, V, Z be set ;
let f be PartFunc of X,Y;
let g be PartFunc of V,Z;
:: original:*
redefine funcg * f ->  PartFunc of X,Z;
coherence
 f * g is PartFunc of X,Z
proofend;
end;

theorem :: PARTFUN1:6
for X, Y being set
for f being Relation of X,Y holds (id X) * f = f
proofend;

theorem :: PARTFUN1:7
for X, Y being set
for f being Relation of X,Y holds f * (id Y) = f
proofend;

theorem :: PARTFUN1:8
for X, Y being set
for f being PartFunc of X,Y st ( for x1, x2 being Element of X st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2 ) holds
f is one-to-one
proofend;

theorem :: PARTFUN1:9
for X, Y being set
for f being PartFunc of X,Y st f is one-to-one holds
f " is PartFunc of Y,X
proofend;

theorem :: PARTFUN1:10
for X, Y, Z being set
for f being PartFunc of X,Y holds f | Z is PartFunc of Z,Y
proofend;

theorem Th11: :: PARTFUN1:11
for X, Y, Z being set
for f being PartFunc of X,Y holds f | Z is PartFunc of X,Y ;

definition
let X, Y be set ;
let f be PartFunc of X,Y;
let Z be set ;
:: original:|
redefine funcf | Z ->  PartFunc of X,Y;
coherence
 f | Z is PartFunc of X,Y by Th11;
end;

theorem :: PARTFUN1:12
for X, Y, Z being set
for f being PartFunc of X,Y holds Z |` f is PartFunc of X,Z
proofend;

theorem :: PARTFUN1:13
for X, Y, Z being set
for f being PartFunc of X,Y holds Z |` f is PartFunc of X,Y ;

theorem Th14: :: PARTFUN1:14
for Y, X being set
for f being Function holds (Y |` f) | X is PartFunc of X,Y
proofend;

theorem :: PARTFUN1:15
for X, Y, y being set
for f being PartFunc of X,Y st y in f .: X holds
ex x being Element of X st
( x in dom f & y = f . x )
proofend;

:: Partial function from a singelton into set
theorem Th16: :: PARTFUN1:16
for x, Y being set
for f being PartFunc of {x},Y holds rng f c= {(f . x)}
proofend;

theorem :: PARTFUN1:17
for x, Y being set
for f being PartFunc of {x},Y holds f is one-to-one
proofend;

theorem :: PARTFUN1:18
for x, Y, P being set
for f being PartFunc of {x},Y holds f .: P c= {(f . x)}
proofend;

theorem :: PARTFUN1:19
for x, X, Y being set
for f being Function st dom f = {x} & x in X & f . x in Y holds
f is PartFunc of X,Y
proofend;

:: Partial function from a set into a singelton
theorem Th20: :: PARTFUN1:20
for X, y, x being set
for f being PartFunc of X,{y} st x in dom f holds
f . x = y
proofend;

theorem :: PARTFUN1:21
for X, y being set
for f1, f2 being PartFunc of X,{y} st dom f1 = dom f2 holds
f1 = f2
proofend;

:: Construction of a Partial Function from a Function
definition
let f be Function;
let X, Y be set ;
func<:f,X,Y:> ->  PartFunc of X,Y equals :: PARTFUN1:def 1
(Y |` f) | X;
coherence
 (Y |` f) | X is PartFunc of X,Y by Th14;
end;

:: deftheorem  defines <: PARTFUN1:def_1_:_
 for f being Function
for X, Y being set holds <:f,X,Y:> = (Y |` f) | X;

theorem Th22: :: PARTFUN1:22
for X, Y being set
for f being Function holds <:f,X,Y:> c= f
proofend;

theorem Th23: :: PARTFUN1:23
for X, Y being set
for f being Function holds
( dom <:f,X,Y:> c= dom f &amp; rng <:f,X,Y:> c= rng f )
proofend;

theorem Th24: :: PARTFUN1:24
for x, X, Y being set
for f being Function holds
( x in dom <:f,X,Y:> iff ( x in dom f &amp; x in X &amp; f . x in Y ) )
proofend;

theorem Th25: :: PARTFUN1:25
for x, X, Y being set
for f being Function st x in dom f &amp; x in X &amp; f . x in Y holds
<:f,X,Y:> . x = f . x
proofend;

theorem Th26: :: PARTFUN1:26
for x, X, Y being set
for f being Function st x in dom <:f,X,Y:> holds
<:f,X,Y:> . x = f . x
proofend;

theorem :: PARTFUN1:27
for X, Y being set
for f, g being Function st f c= g holds
<:f,X,Y:> c= <:g,X,Y:>
proofend;

theorem Th28: :: PARTFUN1:28
for Z, X, Y being set
for f being Function st Z c= X holds
<:f,Z,Y:> c= <:f,X,Y:>
proofend;

theorem Th29: :: PARTFUN1:29
for Z, Y, X being set
for f being Function st Z c= Y holds
<:f,X,Z:> c= <:f,X,Y:>
proofend;

theorem :: PARTFUN1:30
for X1, X2, Y1, Y2 being set
for f being Function st X1 c= X2 &amp; Y1 c= Y2 holds
<:f,X1,Y1:> c= <:f,X2,Y2:>
proofend;

theorem Th31: :: PARTFUN1:31
for X, Y being set
for f being Function st dom f c= X &amp; rng f c= Y holds
f = <:f,X,Y:>
proofend;

theorem :: PARTFUN1:32
for f being Function holds f = <:f,(dom f),(rng f):> ;

theorem :: PARTFUN1:33
for X, Y being set
for f being PartFunc of X,Y holds <:f,X,Y:> = f
proofend;

theorem Th34: :: PARTFUN1:34
for X, Y being set holds <:{},X,Y:> = {}
proofend;

theorem Th35: :: PARTFUN1:35
for Y, Z, X being set
for f, g being Function holds <:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:>
proofend;

theorem :: PARTFUN1:36
for Y, Z, X being set
for f, g being Function st (rng f) /\ (dom g) c= Y holds
<:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:>
proofend;

theorem Th37: :: PARTFUN1:37
for X, Y being set
for f being Function st f is one-to-one holds
<:f,X,Y:> is one-to-one
proofend;

theorem :: PARTFUN1:38
for X, Y being set
for f being Function st f is one-to-one holds
<:f,X,Y:> " = <:(f "),Y,X:>
proofend;

theorem :: PARTFUN1:39
for Z, X, Y being set
for f being Function holds Z |` <:f,X,Y:> = <:f,X,(Z /\ Y):>
proofend;

:: Total Function
definition
let X be set ;
let f be X -defined Relation;
attrf is total  means :Def2: :: PARTFUN1:def 2
 dom f = X;
end;

:: deftheorem Def2 defines total PARTFUN1:def_2_:_
 for X being set
for f being b1 -defined Relation holds
( f is total iff dom f = X );

registration
let X be empty set ;
let Y be set ;
cluster  ->  total for Element of bool [:X,Y:];
coherence
 for b1 being Relation of X,Y holds b1 is total
proofend;
end;

registration
let X be non empty set ;
let Y be empty set ;
cluster  ->  non total for Element of bool [:X,Y:];
coherence
 for b1 being Relation of X,Y holds not b1 is total
proofend;
end;

theorem Th40: :: PARTFUN1:40
for X, Y being set
for f being Function st <:f,X,Y:> is total holds
X c= dom f
proofend;

theorem :: PARTFUN1:41
for X, Y being set st <:{},X,Y:> is total holds
X = {}
proofend;

theorem :: PARTFUN1:42
for X, Y being set
for f being Function st X c= dom f &amp; rng f c= Y holds
<:f,X,Y:> is total
proofend;

theorem :: PARTFUN1:43
for X, Y being set
for f being Function st <:f,X,Y:> is total holds
f .: X c= Y
proofend;

theorem :: PARTFUN1:44
for X, Y being set
for f being Function st X c= dom f &amp; f .: X c= Y holds
<:f,X,Y:> is total
proofend;

:: set of partial functions from a set into a set
definition
let X, Y be set ;
func PFuncs (X,Y) ->  set  means :Def3: :: PARTFUN1:def 3
 for x being set holds
( x in it iff ex f being Function st
( x = f &amp; dom f c= X &amp; rng f c= Y ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex f being Function st
( x = f &amp; dom f c= X &amp; rng f c= Y ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex f being Function st
( x = f &amp; dom f c= X &amp; rng f c= Y ) ) ) &amp; ( for x being set holds
( x in b2 iff ex f being Function st
( x = f &amp; dom f c= X &amp; rng f c= Y ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines PFuncs PARTFUN1:def_3_:_
 for X, Y, b3 being set holds
( b3 = PFuncs (X,Y) iff for x being set holds
( x in b3 iff ex f being Function st
( x = f &amp; dom f c= X &amp; rng f c= Y ) ) );

registration
let X, Y be set ;
cluster PFuncs (X,Y) ->  non empty ;
coherence
 not PFuncs (X,Y) is empty
proofend;
end;

theorem Th45: :: PARTFUN1:45
for X, Y being set
for f being PartFunc of X,Y holds f in PFuncs (X,Y)
proofend;

theorem Th46: :: PARTFUN1:46
for X, Y, f being set st f in PFuncs (X,Y) holds
f is PartFunc of X,Y
proofend;

theorem :: PARTFUN1:47
for X, Y being set
for f being Element of PFuncs (X,Y) holds f is PartFunc of X,Y by Th46;

theorem :: PARTFUN1:48
for Y being set holds PFuncs ({},Y) = {{}}
proofend;

theorem :: PARTFUN1:49
for X being set holds PFuncs (X,{}) = {{}}
proofend;

theorem :: PARTFUN1:50
for X1, X2, Y1, Y2 being set st X1 c= X2 &amp; Y1 c= Y2 holds
PFuncs (X1,Y1) c= PFuncs (X2,Y2)
proofend;

:: Relation of Tolerance on Functions
definition
let f, g be Function;
predf tolerates g means :Def4: :: PARTFUN1:def 4
 for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x;
reflexivity
 for f being Function
for x being set st x in (dom f) /\ (dom f) holds
f . x = f . x ;
symmetry
 for f, g being Function st ( for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x ) holds
for x being set st x in (dom g) /\ (dom f) holds
g . x = f . x ;
end;

:: deftheorem Def4 defines tolerates PARTFUN1:def_4_:_
 for f, g being Function holds
( f tolerates g iff for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x );

theorem Th51: :: PARTFUN1:51
for f, g being Function holds
( f tolerates g iff ex h being Function st f \/ g = h )
proofend;

theorem Th52: :: PARTFUN1:52
for f, g being Function holds
( f tolerates g iff ex h being Function st
( f c= h &amp; g c= h ) )
proofend;

theorem Th53: :: PARTFUN1:53
for f, g being Function st dom f c= dom g holds
( f tolerates g iff for x being set st x in dom f holds
f . x = g . x )
proofend;

theorem :: PARTFUN1:54
for f, g being Function st f c= g holds
f tolerates g by Th52;

theorem Th55: :: PARTFUN1:55
for f, g being Function st dom f = dom g &amp; f tolerates g holds
f = g
proofend;

theorem :: PARTFUN1:56
for f, g being Function st dom f misses dom g holds
f tolerates g
proofend;

theorem :: PARTFUN1:57
for f, g, h being Function st f c= h &amp; g c= h holds
f tolerates g by Th52;

theorem :: PARTFUN1:58
for X, Y being set
for f, g being PartFunc of X,Y
for h being Function st f tolerates h &amp; g c= f holds
g tolerates h
proofend;

theorem Th59: :: PARTFUN1:59
for f being Function holds {} tolerates f
proofend;

theorem :: PARTFUN1:60
for X, Y being set
for f being Function holds <:{},X,Y:> tolerates f
proofend;

theorem :: PARTFUN1:61
for X, y being set
for f, g being PartFunc of X,{y} holds f tolerates g
proofend;

theorem :: PARTFUN1:62
for X being set
for f being Function holds f | X tolerates f
proofend;

theorem :: PARTFUN1:63
for Y being set
for f being Function holds Y |` f tolerates f
proofend;

theorem Th64: :: PARTFUN1:64
for Y, X being set
for f being Function holds (Y |` f) | X tolerates f
proofend;

theorem :: PARTFUN1:65
for X, Y being set
for f being Function holds <:f,X,Y:> tolerates f by Th64;

theorem Th66: :: PARTFUN1:66
for X, Y being set
for f, g being PartFunc of X,Y st f is total &amp; g is total &amp; f tolerates g holds
f = g
proofend;

theorem Th67: :: PARTFUN1:67
for X, Y being set
for f, g, h being PartFunc of X,Y st f tolerates h &amp; g tolerates h &amp; h is total holds
f tolerates g
proofend;

theorem Th68: :: PARTFUN1:68
for X, Y being set
for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) &amp; f tolerates g holds
ex h being PartFunc of X,Y st
( h is total &amp; f tolerates h &amp; g tolerates h )
proofend;

definition
let X, Y be set ;
let f be PartFunc of X,Y;
func TotFuncs f ->  set  means :Def5: :: PARTFUN1:def 5
 for x being set holds
( x in it iff ex g being PartFunc of X,Y st
( g = x &amp; g is total &amp; f tolerates g ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex g being PartFunc of X,Y st
( g = x &amp; g is total &amp; f tolerates g ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex g being PartFunc of X,Y st
( g = x &amp; g is total &amp; f tolerates g ) ) ) &amp; ( for x being set holds
( x in b2 iff ex g being PartFunc of X,Y st
( g = x &amp; g is total &amp; f tolerates g ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines TotFuncs PARTFUN1:def_5_:_
 for X, Y being set
for f being PartFunc of X,Y
for b4 being set holds
( b4 = TotFuncs f iff for x being set holds
( x in b4 iff ex g being PartFunc of X,Y st
( g = x &amp; g is total &amp; f tolerates g ) ) );

theorem Th69: :: PARTFUN1:69
for X, Y being set
for f being PartFunc of X,Y
for g being set st g in TotFuncs f holds
g is PartFunc of X,Y
proofend;

theorem Th70: :: PARTFUN1:70
for X, Y being set
for f, g being PartFunc of X,Y st g in TotFuncs f holds
g is total
proofend;

theorem Th71: :: PARTFUN1:71
for X, Y being set
for f being PartFunc of X,Y
for g being Function st g in TotFuncs f holds
f tolerates g
proofend;

registration
let X be non empty set ;
let Y be empty set ;
let f be PartFunc of X,Y;
cluster TotFuncs f ->  empty ;
coherence
 TotFuncs f is empty
proofend;
end;

theorem Th72: :: PARTFUN1:72
for X, Y being set
for f being PartFunc of X,Y holds
( f is total iff TotFuncs f = {f} )
proofend;

theorem :: PARTFUN1:73
for Y being set
for f being PartFunc of {},Y holds TotFuncs f = {f} by Th72;

theorem :: PARTFUN1:74
for Y being set
for f being PartFunc of {},Y holds TotFuncs f = {{}} by Th72;

theorem :: PARTFUN1:75
for X, Y being set
for f, g being PartFunc of X,Y st TotFuncs f meets TotFuncs g holds
f tolerates g
proofend;

theorem :: PARTFUN1:76
for X, Y being set
for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) &amp; f tolerates g holds
TotFuncs f meets TotFuncs g
proofend;

begin

Lm2:  for X being set
for R being Relation of X st R = id X holds
R is total
proofend;

Lm3:  for X being set
for R being Relation st R = id X holds
( R is reflexive &amp; R is symmetric &amp; R is antisymmetric &amp; R is transitive )
proofend;

Lm4:  for X being set holds id X is Relation of X
proofend;

registration
let X be set ;
cluster Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive total for Element of bool [:X,X:];
existence
 ex b1 being Relation of X st
( b1 is total &amp; b1 is reflexive &amp; b1 is symmetric &amp; b1 is antisymmetric &amp; b1 is transitive )
proofend;
end;

registration
cluster Relation-like symmetric transitive  ->  reflexive for set ;
coherence
 for b1 being Relation st b1 is symmetric &amp; b1 is transitive holds
b1 is reflexive
proofend;
end;

registration
let X be set ;
cluster id X ->  symmetric antisymmetric transitive ;
coherence
 ( id X is symmetric &amp; id X is antisymmetric &amp; id X is transitive ) by Lm3;
end;

definition
let X be set ;
:: original:id
redefine func id X ->  total Relation of X;
coherence
 id X is total Relation of X by Lm2, Lm4;
end;

scheme :: PARTFUN1:sch 4
LambdaC9{ F1() ->  non empty set , P1[ set ], F2( set ) ->  set , F3( set ) ->  set } :
 ex f being Function st
( dom f = F1() &amp; ( for x being Element of F1() holds
( ( P1[x] implies f . x = F2(x) ) &amp; ( P1[x] implies f . x = F3(x) ) ) ) )
proofend;

begin

theorem Th77: :: PARTFUN1:77
for x, y, z being set
for f, g being Function st f tolerates g &amp; [x,y] in f &amp; [x,z] in g holds
y = z
proofend;

theorem :: PARTFUN1:78
for A being set st A is functional &amp; ( for f, g being Function st f in A &amp; g in A holds
f tolerates g ) holds
union A is Function
proofend;

:: Moved from FINSEQ_4 by AK on 2007.10.09
definition
let D be set ;
let p be D -valued Function;
let i be set ;
assume A1: i in dom p ;
funcp /. i ->  Element of D equals :Def6: :: PARTFUN1:def 6
p . i;
coherence
 p . i is Element of D by A1, Th4;
end;

:: deftheorem Def6 defines /. PARTFUN1:def_6_:_
 for D being set
for p being b1 -valued Function
for i being set st i in dom p holds
p /. i = p . i;

:: missing, 2008.09.15, A.T.
registration
let X, Y be non empty set ;
cluster Relation-like X -defined Y -valued Function-like non empty for Element of bool [:X,Y:];
existence
 not for b1 being PartFunc of X,Y holds b1 is empty
proofend;
end;

:: from FRAENKEL, 2009.05.06, A.K.
registration
let A, B be set ;
cluster PFuncs (A,B) ->  functional ;
coherence
 PFuncs (A,B) is functional
proofend;
end;

:: from CIRCCOMB, 2011.04.19, A.T.
theorem :: PARTFUN1:79
for f1, f2, g being Function st rng g c= dom f1 &amp; rng g c= dom f2 &amp; f1 tolerates f2 holds
f1 * g = f2 * g
proofend;

:: missing, 2011.06.06, A.T.
theorem :: PARTFUN1:80
for Y, x, X being set
for f being b1 -valued Function st x in dom (f | X) holds
(f | X) /. x = f /. x
proofend;