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

:: Auxiliary theorems

theorem Th1: :: PARTFUN1:1

for f, g being Function st ( for x being object st x in (dom f) /\ (dom g) holds
f . x = g . x ) holds
f \/ g is Function

proof end;

theorem Th2: :: PARTFUN1:2

for f, g, h being Function st f \/ g = h holds
for x being object st x in (dom f) /\ (dom g) holds
f . x = g . x

proof end;

scheme :: PARTFUN1:sch 1
LambdaC{ F₁() -> set , P₁[ object ], F₂( object ) -> object , F₃( object ) -> object } :

ex f being Function st
( dom f = F₁() & ( for x being object st x in F₁() holds
( ( P₁[x] implies f . x = F₂(x) ) & ( P₁[x] implies f . x = F₃(x) ) ) ) )

proof end;

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 ) ; :: 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 b₁ being Relation of X,Y st b₁ is Function-like

proof end;

end;

definition

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

end;

theorem :: PARTFUN1:3

for y being object
for X, 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 )

proof end;

theorem Th4: :: PARTFUN1:4

for x being object
for Y being set
for f being b₂ -valued Function st x in dom f holds
f . x in Y

proof end;

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 ;

scheme :: PARTFUN1:sch 2
PartFuncEx{ F₁() -> set , F₂() -> set , P₁[ object , object ] } :

ex f being PartFunc of F₁(),F₂() st
( ( for x being object holds
( x in dom f iff ( x in F₁() & ex y being object st P₁[x,y] ) ) ) & ( for x being object st x in dom f holds
P₁[x,f . x] ) )

provided

A1: for x, y being object st x in F₁() & P₁[x,y] holds
y in F₂() and
A2: for x, y1, y2 being object st x in F₁() & P₁[x,y1] & P₁[x,y2] holds
y1 = y2

proof end;

scheme :: PARTFUN1:sch 3
LambdaR{ F₁() -> set , F₂() -> set , F₃( object ) -> object , P₁[ object ] } :

ex f being PartFunc of F₁(),F₂() st
( ( for x being object holds
( x in dom f iff ( x in F₁() & P₁[x] ) ) ) & ( for x being object st x in dom f holds
f . x = F₃(x) ) )

provided

A1: for x being object st P₁[x] holds
F₃(x) in F₂()

proof end;

definition

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

proof end;

end;

theorem :: PARTFUN1:6

for X, Y being set
for f being Relation of X,Y holds (id X) * f = f

proof end;

theorem :: PARTFUN1:7

for X, Y being set
for f being Relation of X,Y holds f * (id Y) = f

proof end;

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 ;

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

proof end;

theorem :: PARTFUN1:10

for X, Y, Z being set
for f being PartFunc of X,Y holds f | Z is PartFunc of Z,Y

proof end;

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 func f | 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

proof end;

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 X, Y being set
for f being Function holds (Y |` f) | X is PartFunc of X,Y

proof end;

theorem :: PARTFUN1:15

for y being object
for X, 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 )

proof end;

:: Partial function from a singelton into set

theorem Th16: :: PARTFUN1:16

for x being object
for Y being set
for f being PartFunc of {x},Y holds rng f c= {(f . x)}

proof end;

theorem :: PARTFUN1:17

for x being object
for Y being set
for f being PartFunc of {x},Y holds f is one-to-one

proof end;

theorem :: PARTFUN1:18

for x being object
for P, Y being set
for f being PartFunc of {x},Y holds f .: P c= {(f . x)}

proof end;

theorem :: PARTFUN1:19

for x being object
for 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

proof end;

:: Partial function from a set into a singelton

theorem Th20: :: PARTFUN1:20

for x, y being object
for X being set
for f being PartFunc of X,{y} st x in dom f holds
f . x = y

proof end;

theorem :: PARTFUN1:21

for y being object
for X being set
for f1, f2 being PartFunc of X,{y} st dom f1 = dom f2 holds
f1 = f2

proof end;

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

proof end;

theorem Th23: :: PARTFUN1:23

for X, Y being set
for f being Function holds
( dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f )

proof end;

theorem Th24: :: PARTFUN1:24

for x being object
for X, Y being set
for f being Function holds
( x in dom <:f,X,Y:> iff ( x in dom f & x in X & f . x in Y ) )

proof end;

theorem Th25: :: PARTFUN1:25

for x being object
for X, Y being set
for f being Function st x in dom f & x in X & f . x in Y holds
<:f,X,Y:> . x = f . x

proof end;

theorem Th26: :: PARTFUN1:26

for x being object
for X, Y being set
for f being Function st x in dom <:f,X,Y:> holds
<:f,X,Y:> . x = f . x

proof end;

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

proof end;

theorem Th28: :: PARTFUN1:28

for X, Y, Z being set
for f being Function st Z c= X holds
<:f,Z,Y:> c= <:f,X,Y:>

proof end;

theorem Th29: :: PARTFUN1:29

for X, Y, Z being set
for f being Function st Z c= Y holds
<:f,X,Z:> c= <:f,X,Y:>

proof end;

theorem :: PARTFUN1:30

for X1, X2, Y1, Y2 being set
for f being Function st X1 c= X2 & Y1 c= Y2 holds
<:f,X1,Y1:> c= <:f,X2,Y2:>

proof end;

theorem Th31: :: PARTFUN1:31

for X, Y being set
for f being Function st dom f c= X & rng f c= Y holds
f = <:f,X,Y:>

proof end;

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 ;

theorem Th34: :: PARTFUN1:34

for X, Y being set holds <:{},X,Y:> = {}

proof end;

theorem Th35: :: PARTFUN1:35

for X, Y, Z being set
for f, g being Function holds <:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:>

proof end;

theorem :: PARTFUN1:36

for X, Y, Z 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:>

proof end;

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

proof end;

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

proof end;

theorem :: PARTFUN1:39

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

proof end;

:: Total Function

definition

let X be set ;
let f be X -defined Relation;

attr f is total means :: PARTFUN1:def 2
dom f = X;

end;

:: deftheorem defines total PARTFUN1:def 2 :
for X being set
for f being b₁ -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 b₁ being Relation of X,Y holds b₁ is total ;

end;

registration

let X be non empty set ;
let Y be empty set ;

cluster -> non total for Element of bool [:X,Y:];

coherence
for b₁ being Relation of X,Y holds not b₁ is total ;

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 by Th23;

theorem :: PARTFUN1:41

for X, Y being set st <:{},X,Y:> is total holds
X = {}

proof end;

theorem :: PARTFUN1:42

for X, Y being set
for f being Function st X c= dom f & rng f c= Y holds
<:f,X,Y:> is total

proof end;

theorem :: PARTFUN1:43

for X, Y being set
for f being Function st <:f,X,Y:> is total holds
f .: X c= Y

proof end;

theorem :: PARTFUN1:44

for X, Y being set
for f being Function st X c= dom f & f .: X c= Y holds
<:f,X,Y:> is total

proof end;

:: 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 object holds
( x in it iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) ) ) & ( for x being object holds
( x in b₂ iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines PFuncs PARTFUN1:def 3 :
for X, Y, b₃ being set holds
( b₃ = PFuncs (X,Y) iff for x being object holds
( x in b₃ iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) ) );

registration

let X, Y be set ;

cluster PFuncs (X,Y) -> non empty ;

coherence
not PFuncs (X,Y) is empty

proof end;

end;

theorem Th45: :: PARTFUN1:45

for X, Y being set
for f being PartFunc of X,Y holds f in PFuncs (X,Y)

proof end;

theorem Th46: :: PARTFUN1:46

for X, Y, f being set st f in PFuncs (X,Y) holds
f is PartFunc of X,Y

proof end;

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) = {{}}

proof end;

theorem :: PARTFUN1:49

for X being set holds PFuncs (X,{}) = {{}}

proof end;

theorem :: PARTFUN1:50

for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds
PFuncs (X1,Y1) c= PFuncs (X2,Y2)

proof end;

:: Relation of Tolerance on Functions

definition

let f, g be Function;

pred f tolerates g means :: PARTFUN1:def 4
for x being object st x in (dom f) /\ (dom g) holds
f . x = g . x;

reflexivity
for f being Function
for x being object st x in (dom f) /\ (dom f) holds
f . x = f . x ;
symmetry
for f, g being Function st ( for x being object st x in (dom f) /\ (dom g) holds
f . x = g . x ) holds
for x being object st x in (dom g) /\ (dom f) holds
g . x = f . x ;

end;

:: deftheorem defines tolerates PARTFUN1:def 4 :
for f, g being Function holds
( f tolerates g iff for x being object 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 f \/ g is Function ) by Th1, Th2;

theorem Th52: :: PARTFUN1:52

for f, g being Function holds
( f tolerates g iff ex h being Function st
( f c= h & g c= h ) )

proof end;

theorem :: PARTFUN1:53

for f, g being Function st dom f c= dom g holds
( f tolerates g iff for x being object st x in dom f holds
f . x = g . x )

proof end;

theorem :: PARTFUN1:54

for f, g being Function st f c= g holds
f tolerates g by Th52;

theorem :: PARTFUN1:55

for f, g being Function st dom f = dom g & f tolerates g holds
f = g ;

theorem :: PARTFUN1:56

for f, g being Function st dom f misses dom g holds
f tolerates g ;

theorem :: PARTFUN1:57

for f, g, h being Function st f c= h & 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 & g c= f holds
g tolerates h

proof end;

theorem :: PARTFUN1:59

for f being Function holds {} tolerates f ;

theorem :: PARTFUN1:60

for X, Y being set
for f being Function holds <:{},X,Y:> tolerates f

proof end;

theorem :: PARTFUN1:61

for y being object
for X being set
for f, g being PartFunc of X,{y} holds f tolerates g

proof end;

theorem :: PARTFUN1:62

for X being set
for f being Function holds f | X tolerates f

proof end;

theorem :: PARTFUN1:63

for Y being set
for f being Function holds Y |` f tolerates f

proof end;

theorem Th64: :: PARTFUN1:64

for X, Y being set
for f being Function holds (Y |` f) | X tolerates f

proof end;

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 & g is total & f tolerates g holds
f = g ;

theorem Th67: :: PARTFUN1:67

for X, Y being set
for f, g, h being PartFunc of X,Y st f tolerates h & g tolerates h & h is total holds
f tolerates g

proof end;

theorem Th68: :: PARTFUN1:68

for X, Y being set
for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds
ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h )

proof end;

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 object holds
( x in it iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) ) & ( for x being object holds
( x in b₂ iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines TotFuncs PARTFUN1:def 5 :
for X, Y being set
for f being PartFunc of X,Y
for b₄ being set holds
( b₄ = TotFuncs f iff for x being object holds
( x in b₄ iff ex g being PartFunc of X,Y st
( g = x & g is total & 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

proof end;

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

proof end;

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

proof end;

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

proof end;

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} )

proof end;

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

proof end;

theorem :: PARTFUN1:76

for X, Y being set
for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds
TotFuncs f meets TotFuncs g

proof end;

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

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

proof end;

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

proof end;

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 b₁ being Relation of X st
( b₁ is total & b₁ is reflexive & b₁ is symmetric & b₁ is antisymmetric & b₁ is transitive )

proof end;

end;

registration

cluster Relation-like symmetric transitive -> reflexive for set ;

coherence
for b₁ being Relation st b₁ is symmetric & b₁ is transitive holds
b₁ is reflexive

proof end;

end;

registration

let X be set ;

cluster id X -> symmetric antisymmetric transitive ;

coherence
( id X is symmetric & id X is antisymmetric & 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{ F₁() -> non empty set , P₁[ object ], F₂( object ) -> object , F₃( object ) -> object } :

ex f being Function st
( dom f = F₁() & ( for x being Element of F₁() holds
( ( P₁[x] implies f . x = F₂(x) ) & ( P₁[x] implies f . x = F₃(x) ) ) ) )

proof end;

theorem Th77: :: PARTFUN1:77

for f, g being Function
for x, y, z being object st f tolerates g & [x,y] in f & [x,z] in g holds
y = z

proof end;

theorem :: PARTFUN1:78

for A being set st A is functional & ( for f, g being Function st f in A & g in A holds
f tolerates g ) holds
union A is Function

proof end;

:: Moved from FINSEQ_4 by AK on 2007.10.09

definition

let D be set ;
let p be D -valued Function;
let i be object ;
assume A1: i in dom p ;

func p /. 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 b₁ -valued Function
for i being object 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 b₁ being PartFunc of X,Y holds b₁ is empty

proof end;

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

proof end;

end;

:: from CIRCCOMB, 2011.04.19, A.T.

theorem :: PARTFUN1:79

for f1, f2, g being Function st rng g c= dom f1 & rng g c= dom f2 & f1 tolerates f2 holds
f1 * g = f2 * g

proof end;

:: missing, 2011.06.06, A.T.

theorem :: PARTFUN1:80

for x being object
for X, Y being set
for f being b₃ -valued Function st x in dom (f | X) holds
(f | X) /. x = f /. x

proof end;

scheme :: PARTFUN1:sch 5
LambdaCS{ F₁() -> set , P₁[ object ], F₂( object ) -> object , F₃( object ) -> object } :

ex f being Function st
( dom f = F₁() & ( for x being set st x in F₁() holds
( ( P₁[x] implies f . x = F₂(x) ) & ( P₁[x] implies f . x = F₃(x) ) ) ) )

proof end;

theorem :: PARTFUN1:81

for x being object
for f, g being Function st f . x = g . x holds
f | {x} tolerates g | {x}

proof end;

theorem :: PARTFUN1:82

for x, y being object
for f, g being Function st f . x = g . x & f . y = g . y holds
f | {x,y} tolerates g | {x,y}

proof end;

definition

let A, B be set ;
let F be PFuncs (A,B) -valued Function;
let i be object ;
:: original: .
redefine func F . i -> PartFunc of A,B;
coherence
F . i is PartFunc of A,B

proof end;

end;