:: PARTFUN1 semantic presentation

theorem Th1: :: PARTFUN1:1

for P, X1, Y1, Q, X2, Y2 being set st P c= [:X1,Y1:] & Q c= [:X2,Y2:] holds
P \/ Q c= [:(X1 \/ X2),(Y1 \/ Y2):]

proof end;

theorem Th2: :: PARTFUN1:2

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

proof end;

theorem Th3: :: PARTFUN1:3

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

proof end;

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

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;

registration

cluster empty set ;
existence

proof end;

end;

Lm1: dom {} = {}
;

theorem :: PARTFUN1:4

canceled;

theorem :: PARTFUN1:5

canceled;

theorem :: PARTFUN1:6

canceled;

theorem :: PARTFUN1:7

canceled;

theorem :: PARTFUN1:8

canceled;

theorem :: PARTFUN1:9

canceled;

theorem :: PARTFUN1:10

rng {} = {} ;

Lm2: now

let X, Y be set ;
take E = {} ; :: thesis:
thus ( dom E c= X & rng E c= Y ) by XBOOLE_1:2; :: thesis:

end;

Lm3: for X, Y being set
for R being Relation holds
( R is Relation of X,Y iff ( dom R c= X & rng R c= Y ) )
by RELSET_1:11, RELSET_1:12;

registration

let X, Y be set ;
cluster Function-like Relation of X,Y;
existence

proof end;

end;

definition

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

end;

theorem :: PARTFUN1:11

canceled;

theorem :: PARTFUN1:12

canceled;

theorem :: PARTFUN1:13

canceled;

theorem :: PARTFUN1:14

canceled;

theorem :: PARTFUN1:15

canceled;

theorem :: PARTFUN1:16

canceled;

theorem :: PARTFUN1:17

canceled;

theorem :: PARTFUN1:18

canceled;

theorem :: PARTFUN1:19

canceled;

theorem :: PARTFUN1:20

canceled;

theorem :: PARTFUN1:21

canceled;

theorem :: PARTFUN1:22

canceled;

theorem :: PARTFUN1:23

canceled;

theorem :: PARTFUN1:24

for f being Function holds f is PartFunc of dom f, rng f by Lm3;

theorem :: PARTFUN1:25

for Y being set
for f being Function st rng f c= Y holds
f is PartFunc of dom f,Y by Lm3;

theorem :: PARTFUN1:26

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 )

proof end;

theorem Th27: :: PARTFUN1:27

for X, Y, x being set
for f being PartFunc of X,Y st x in dom f holds
f . x in Y

proof end;

theorem :: PARTFUN1:28

for X, Y, Z being set
for f being PartFunc of X,Y st dom f c= Z holds
f is PartFunc of Z,Y

proof end;

theorem :: PARTFUN1:29

for X, Y, Z being set
for f being PartFunc of X,Y st rng f c= Z holds
f is PartFunc of X,Z

proof end;

theorem Th30: :: PARTFUN1:30

for X, Y, Z being set
for f being PartFunc of X,Y st X c= Z holds
f is PartFunc of Z,Y

proof end;

theorem Th31: :: PARTFUN1:31

for X, Y, Z being set
for f being PartFunc of X,Y st Y c= Z holds
f is PartFunc of X,Z

proof end;

theorem Th32: :: PARTFUN1:32

for X1, Y1, X2, Y2 being set
for f being PartFunc of X1,Y1 st X1 c= X2 & Y1 c= Y2 holds
f is PartFunc of X2,Y2

proof end;

theorem :: PARTFUN1:33

for X, Y being set
for f being Function
for g being PartFunc of X,Y st f c= g holds
f is PartFunc of X,Y

proof end;

theorem :: PARTFUN1:34

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

proof end;

theorem :: PARTFUN1:35

for X, Y, Z being set
for f1, f2 being PartFunc of [:X,Y:],Z st dom f1 = dom f2 & ( for x, y being set st [x,y] in dom f1 holds
f1 . [x,y] = f2 . [x,y] ) holds
f1 = f2

proof end;

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

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

provided

A1: for x, y being set st x in F₁() & P₁[x,y] holds
y in F₂() and
A2: for x, y1, y2 being set 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₃( set ) -> set , P₁[ set ] } :

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

provided

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

proof end;

scheme :: PARTFUN1:sch 4
PartFuncEx2{ F₁() -> set , F₂() -> set , F₃() -> set , P₁[ set , set , set ] } :

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

provided

A1: for x, y, z being set st x in F₁() & y in F₂() & P₁[x,y,z] holds
z in F₃() and
A2: for x, y, z1, z2 being set st x in F₁() & y in F₂() & P₁[x,y,z1] & P₁[x,y,z2] holds
z1 = z2

proof end;

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

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

provided

A1: for x, y being set st P₁[x,y] holds
F₄(x,y) 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

proof end;

end;

theorem :: PARTFUN1:36

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

proof end;

theorem :: PARTFUN1:37

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

proof end;

theorem :: PARTFUN1:38

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

proof end;

theorem :: PARTFUN1:39

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

canceled;

theorem :: PARTFUN1:41

canceled;

theorem :: PARTFUN1:42

canceled;

theorem :: PARTFUN1:43

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

proof end;

theorem Th44: :: PARTFUN1:44

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

end;

theorem :: PARTFUN1:45

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

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

theorem Th47: :: PARTFUN1:47

for Y, X being set
for f being Function holds (Y | f) | X is PartFunc of X,Y

proof end;

theorem :: PARTFUN1:48

canceled;

theorem :: PARTFUN1:49

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 )

proof end;

theorem :: PARTFUN1:50

canceled;

theorem :: PARTFUN1:51

for X, Y being set
for f being PartFunc of X,Y holds f .: X = rng f

proof end;

theorem :: PARTFUN1:52

canceled;

theorem :: PARTFUN1:53

for X, Y being set
for f being PartFunc of X,Y holds f " Y = dom f

proof end;

theorem Th54: :: PARTFUN1:54

for Y being set
for f being PartFunc of {} ,Y holds
( dom f = {} & rng f = {} )

proof end;

theorem Th55: :: PARTFUN1:55

for X, Y being set
for f being Function st dom f = {} holds
f is PartFunc of X,Y

proof end;

theorem :: PARTFUN1:56

for X, Y being set holds {} is PartFunc of X,Y by Lm1, Th55;

theorem Th57: :: PARTFUN1:57

for Y being set
for f being PartFunc of {} ,Y holds f = {}

proof end;

theorem :: PARTFUN1:58

for Y1, Y2 being set
for f1 being PartFunc of {} ,Y1
for f2 being PartFunc of {} ,Y2 holds f1 = f2

proof end;

theorem :: PARTFUN1:59

for Y being set
for f being PartFunc of {} ,Y holds f is one-to-one by Th57;

theorem :: PARTFUN1:60

for Y, P being set
for f being PartFunc of {} ,Y holds f .: P = {}

proof end;

theorem :: PARTFUN1:61

for Y, Q being set
for f being PartFunc of {} ,Y holds f " Q = {}

proof end;

theorem Th62: :: PARTFUN1:62

for X being set
for f being PartFunc of X, {} holds
( dom f = {} & rng f = {} )

proof end;

theorem :: PARTFUN1:63

for X, Y being set
for f being Function st rng f = {} holds
f is PartFunc of X,Y

proof end;

theorem Th64: :: PARTFUN1:64

for X being set
for f being PartFunc of X, {} holds f = {}

proof end;

theorem :: PARTFUN1:65

for X1, X2 being set
for f1 being PartFunc of X1, {}
for f2 being PartFunc of X2, {} holds f1 = f2

proof end;

theorem :: PARTFUN1:66

for X being set
for f being PartFunc of X, {} holds f is one-to-one by Th64;

theorem :: PARTFUN1:67

for X, P being set
for f being PartFunc of X, {} holds f .: P = {}

proof end;

theorem :: PARTFUN1:68

for X, Q being set
for f being PartFunc of X, {} holds f " Q = {}

proof end;

theorem Th69: :: PARTFUN1:69

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

proof end;

theorem :: PARTFUN1:70

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

proof end;

theorem :: PARTFUN1:71

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

proof end;

theorem :: PARTFUN1:72

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

proof end;

theorem Th73: :: PARTFUN1:73

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

proof end;

theorem :: PARTFUN1:74

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

proof end;

definition

let f be Function;
let X, Y be set ;
canceled;
canceled;
func <:f,X,Y:> -> PartFunc of X,Y equals :: PARTFUN1:def 3
(Y | f) | X;
coherence by Th47;

end;

:: deftheorem PARTFUN1:def 1 :

:: deftheorem PARTFUN1:def 2 :

:: deftheorem defines <: PARTFUN1:def 3 :

theorem :: PARTFUN1:75

canceled;

theorem Th76: :: PARTFUN1:76

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

proof end;

theorem Th77: :: PARTFUN1:77

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 Th78: :: PARTFUN1:78

for x, 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 Th79: :: PARTFUN1:79

for x, 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 Th80: :: PARTFUN1:80

for x, 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:81

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 Th82: :: PARTFUN1:82

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

proof end;

theorem Th83: :: PARTFUN1:83

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

proof end;

theorem :: PARTFUN1:84

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 Th85: :: PARTFUN1:85

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

for f being Function holds f = <:f,(dom f),(rng f):> by Th85;

theorem :: PARTFUN1:87

for X, Y being set
for f being PartFunc of X,Y holds <:f,X,Y:> = f

proof end;

theorem :: PARTFUN1:88

canceled;

theorem :: PARTFUN1:89

canceled;

theorem :: PARTFUN1:90

canceled;

theorem Th91: :: PARTFUN1:91

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

proof end;

theorem Th92: :: PARTFUN1:92

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

proof end;

theorem :: PARTFUN1:93

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

proof end;

theorem Th94: :: PARTFUN1:94

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

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

for X, Y, Z being set
for f being Function holds <:f,X,Y:> | Z = <:f,(X /\ Z),Y:> by RELAT_1:100;

theorem :: PARTFUN1:97

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

proof end;

definition

let X, Y be set ;
let f be Relation of X,Y;
attr f is total means :Def4: :: PARTFUN1:def 4
dom f = X;

end;

:: deftheorem Def4 defines total PARTFUN1:def 4 :

theorem :: PARTFUN1:98

canceled;

theorem :: PARTFUN1:99

for X, Y being set
for f being PartFunc of X,Y st f is total & Y = {} holds
X = {}

proof end;

theorem :: PARTFUN1:100

canceled;

theorem :: PARTFUN1:101

canceled;

theorem :: PARTFUN1:102

canceled;

theorem :: PARTFUN1:103

canceled;

theorem :: PARTFUN1:104

canceled;

theorem :: PARTFUN1:105

canceled;

theorem :: PARTFUN1:106

canceled;

theorem :: PARTFUN1:107

canceled;

theorem :: PARTFUN1:108

canceled;

theorem :: PARTFUN1:109

canceled;

theorem :: PARTFUN1:110

canceled;

theorem :: PARTFUN1:111

canceled;

theorem Th112: :: PARTFUN1:112

for Y being set
for f being PartFunc of {} ,Y holds f is total

proof end;

theorem Th113: :: PARTFUN1:113

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

proof end;

theorem :: PARTFUN1:114

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

proof end;

theorem :: PARTFUN1:115

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

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

proof end;

theorem :: PARTFUN1:117

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;

definition

let X, Y be set ;
func PFuncs X,Y -> set means :Def5: :: PARTFUN1:def 5
for x being set holds
( x in it iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines PFuncs PARTFUN1:def 5 :

registration

let X, Y be set ;
cluster PFuncs X,Y -> non empty ;
coherence

proof end;

end;

theorem :: PARTFUN1:118

canceled;

theorem Th119: :: PARTFUN1:119

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

proof end;

theorem Th120: :: PARTFUN1:120

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

proof end;

theorem :: PARTFUN1:121

for X, Y being set
for f being Element of PFuncs X,Y holds f is PartFunc of X,Y by Th120;

theorem :: PARTFUN1:122

for Y being set holds PFuncs {} ,Y = {{} }

proof end;

theorem :: PARTFUN1:123

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

proof end;

theorem :: PARTFUN1:124

canceled;

theorem Th125: :: PARTFUN1:125

for Z, X, Y being set st Z c= X holds
PFuncs Z,Y c= PFuncs X,Y

proof end;

theorem :: PARTFUN1:126

for Y, X being set holds PFuncs {} ,Y c= PFuncs X,Y

proof end;

theorem :: PARTFUN1:127

for Z, Y, X being set st Z c= Y holds
PFuncs X,Z c= PFuncs X,Y

proof end;

theorem :: PARTFUN1:128

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

proof end;

definition

let f, g be Function;
pred f tolerates g means :Def6: :: PARTFUN1:def 6
for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x;
reflexivity ;
symmetry ;

end;

:: deftheorem Def6 defines tolerates PARTFUN1:def 6 :

theorem :: PARTFUN1:129

canceled;

theorem Th130: :: PARTFUN1:130

for f, g being Function holds
( f tolerates g iff ex h being Function st f \/ g = h )

proof end;

theorem Th131: :: PARTFUN1:131

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

proof end;

theorem Th132: :: PARTFUN1:132

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 )

proof end;

theorem :: PARTFUN1:133

canceled;

theorem :: PARTFUN1:134

canceled;

theorem :: PARTFUN1:135

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

theorem Th136: :: PARTFUN1:136

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

proof end;

theorem :: PARTFUN1:137

canceled;

theorem :: PARTFUN1:138

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

proof end;

theorem :: PARTFUN1:139

for f, g, h being Function st f c= h & g c= h holds
f tolerates g by Th131;

theorem :: PARTFUN1:140

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 Th141: :: PARTFUN1:141

for f being Function holds {} tolerates f

proof end;

theorem Th142: :: PARTFUN1:142

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

proof end;

theorem :: PARTFUN1:143

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

proof end;

theorem :: PARTFUN1:144

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

proof end;

theorem :: PARTFUN1:145

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

proof end;

theorem Th146: :: PARTFUN1:146

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

proof end;

theorem :: PARTFUN1:147

for X, Y being set
for f being Function holds <:f,X,Y:> tolerates f by Th146;

theorem Th148: :: PARTFUN1:148

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

proof end;

theorem :: PARTFUN1:149

canceled;

theorem :: PARTFUN1:150

canceled;

theorem :: PARTFUN1:151

canceled;

theorem :: PARTFUN1:152

canceled;

theorem :: PARTFUN1:153

canceled;

theorem :: PARTFUN1:154

canceled;

theorem :: PARTFUN1:155

canceled;

theorem :: PARTFUN1:156

canceled;

theorem :: PARTFUN1:157

canceled;

theorem Th158: :: PARTFUN1:158

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

canceled;

theorem :: PARTFUN1:160

canceled;

theorem :: PARTFUN1:161

canceled;

theorem Th162: :: PARTFUN1:162

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 :Def7: :: PARTFUN1:def 7
for x being set holds
( x in it iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) );
existence

proof end;