:: PARTFUN2 semantic presentation

theorem :: PARTFUN2:1

canceled;

theorem :: PARTFUN2:2

canceled;

theorem Th3: :: PARTFUN2:3

for D, C being non empty set
for f, g being PartFunc of C,D st dom f = dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) holds
f = g

proof end;

theorem Th4: :: PARTFUN2:4

for y being set
for D, C being non empty set
for f being PartFunc of C,D holds
( y in rng f iff ex c being Element of C st
( c in dom f & y = f /. c ) )

proof end;

theorem :: PARTFUN2:5

canceled;

theorem Th6: :: PARTFUN2:6

for D, E, C being non empty set
for f being PartFunc of C,D
for s being PartFunc of D,E
for h being PartFunc of C,E holds
( h = s * f iff ( ( for c being Element of C holds
( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds
h /. c = s /. (f /. c) ) ) )

proof end;

theorem :: PARTFUN2:7

canceled;

theorem :: PARTFUN2:8

canceled;

theorem Th9: :: PARTFUN2:9

for C, D, E being non empty set
for c being Element of C
for f being PartFunc of C,D
for s being PartFunc of D,E st c in dom f & f /. c in dom s holds
(s * f) /. c = s /. (f /. c)

proof end;

theorem :: PARTFUN2:10

for C, D, E being non empty set
for c being Element of C
for f being PartFunc of C,D
for s being PartFunc of D,E st rng f c= dom s & c in dom f holds
(s * f) /. c = s /. (f /. c)

proof end;

definition

let D be non empty set ;
let SD be Subset of D;
:: original: id
redefine func id SD -> PartFunc of D,D;
coherence

proof end;

end;

theorem :: PARTFUN2:11

canceled;

theorem Th12: :: PARTFUN2:12

for D being non empty set
for SD being Subset of D
for F being PartFunc of D,D holds
( F = id SD iff ( dom F = SD & ( for d being Element of D st d in SD holds
F /. d = d ) ) )

proof end;

theorem :: PARTFUN2:13

canceled;

theorem :: PARTFUN2:14

for D being non empty set
for SD being Subset of D
for d being Element of D
for F being PartFunc of D,D st d in (dom F) /\ SD holds
F /. d = (F * (id SD)) /. d

proof end;

theorem :: PARTFUN2:15

for D being non empty set
for SD being Subset of D
for d being Element of D
for F being PartFunc of D,D holds
( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) )

proof end;

theorem :: PARTFUN2:16

for D, C being non empty set
for f being PartFunc of C,D st ( for c1, c2 being Element of C st c1 in dom f & c2 in dom f & f /. c1 = f /. c2 holds
c1 = c2 ) holds
f is one-to-one

proof end;

theorem :: PARTFUN2:17

for x, y being set
for C, D being non empty set
for f being PartFunc of C,D st f is one-to-one & x in dom f & y in dom f & f /. x = f /. y holds
x = y

proof end;

registration

cluster {} -> one-to-one ;
coherence ;

end;

registration

let X, Y be set ;
cluster one-to-one Relation of X,Y;
existence

proof end;

end;

definition

let X, Y be set ;
let f be one-to-one PartFunc of X,Y;
:: original: "
redefine func f " -> PartFunc of Y,X;
coherence by PARTFUN1:39;

end;

theorem Th18: :: PARTFUN2:18

for C, D being non empty set
for f being one-to-one PartFunc of C,D
for g being PartFunc of D,C holds
( g = f " iff ( dom g = rng f & ( for d being Element of D
for c being Element of C holds
( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) )

proof end;

theorem :: PARTFUN2:19

canceled;

theorem :: PARTFUN2:20

canceled;

theorem :: PARTFUN2:21

canceled;

theorem :: PARTFUN2:22

for C, D being non empty set
for c being Element of C
for f being one-to-one PartFunc of C,D st c in dom f holds
( c = (f " ) /. (f /. c) & c = ((f " ) * f) /. c )

proof end;

theorem :: PARTFUN2:23

for C, D being non empty set
for d being Element of D
for f being one-to-one PartFunc of C,D st d in rng f holds
( d = f /. ((f " ) /. d) & d = (f * (f " )) /. d )

proof end;

theorem :: PARTFUN2:24

for C, D being non empty set
for f being PartFunc of C,D
for t being PartFunc of D,C st f is one-to-one & dom f = rng t & rng f = dom t & ( for c being Element of C
for d being Element of D st c in dom f & d in dom t holds
( f /. c = d iff t /. d = c ) ) holds
t = f "

proof end;

theorem :: PARTFUN2:25

canceled;

theorem :: PARTFUN2:26

canceled;

theorem :: PARTFUN2:27

canceled;

theorem :: PARTFUN2:28

canceled;

theorem :: PARTFUN2:29

canceled;

theorem :: PARTFUN2:30

canceled;

theorem :: PARTFUN2:31

canceled;

theorem Th32: :: PARTFUN2:32

for X being set
for D, C being non empty set
for g, f being PartFunc of C,D holds
( g = f | X iff ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) )

proof end;

theorem :: PARTFUN2:33

canceled;

theorem Th34: :: PARTFUN2:34

for X being set
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in (dom f) /\ X holds
(f | X) /. c = f /. c

proof end;

theorem :: PARTFUN2:35

for X being set
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in dom f & c in X holds
(f | X) /. c = f /. c

proof end;

theorem :: PARTFUN2:36

for X being set
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in dom f & c in X holds
f /. c in rng (f | X)

proof end;

definition

let C, D be non empty set ;
let X be set ;
let f be PartFunc of C,D;
:: original: |
redefine func X | f -> PartFunc of C,D;
coherence by PARTFUN1:46;

end;

theorem Th37: :: PARTFUN2:37

for X being set
for D, C being non empty set
for g, f being PartFunc of C,D holds
( g = X | f iff ( ( for c being Element of C holds
( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) )

proof end;

theorem :: PARTFUN2:38

for X being set
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D holds
( c in dom (X | f) iff ( c in dom f & f /. c in X ) ) by Th37;

theorem :: PARTFUN2:39

for X being set
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in dom (X | f) holds
(X | f) /. c = f /. c by Th37;

theorem Th40: :: PARTFUN2:40

for X being set
for D, C being non empty set
for SD being Subset of D
for f being PartFunc of C,D holds
( SD = f .: X iff for d being Element of D holds
( d in SD iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) )

proof end;

theorem :: PARTFUN2:41

for X being set
for C, D being non empty set
for d being Element of D
for f being PartFunc of C,D holds
( d in f .: X iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) by Th40;

theorem :: PARTFUN2:42

for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in dom f holds
f .: {c} = {(f /. c)}

proof end;

theorem :: PARTFUN2:43

for C, D being non empty set
for c1, c2 being Element of C
for f being PartFunc of C,D st c1 in dom f & c2 in dom f holds
f .: {c1,c2} = {(f /. c1),(f /. c2)}

proof end;

theorem Th44: :: PARTFUN2:44

for X being set
for D, C being non empty set
for SC being Subset of C
for f being PartFunc of C,D holds
( SC = f " X iff for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) )

proof end;

theorem :: PARTFUN2:45

canceled;

theorem :: PARTFUN2:46

for D, C being non empty set
for f being PartFunc of C,D ex g being Function of C,D st
for c being Element of C st c in dom f holds
g . c = f /. c

proof end;

theorem :: PARTFUN2:47

for D, C being non empty set
for f, g being PartFunc of C,D holds
( f tolerates g iff for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c )

proof end;

scheme :: PARTFUN2:sch 1
PartFuncExD{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set ] } :

ex f being PartFunc of F₁(),F₂() st
( ( for d being Element of F₁() holds
( d in dom f iff ex c being Element of F₂() st P₁[d,c] ) ) & ( for d being Element of F₁() st d in dom f holds
P₁[d,f /. d] ) )

proof end;

scheme :: PARTFUN2:sch 2
LambdaPFD{ F₁() -> non empty set , F₂() -> non empty set , F₃( set ) -> Element of F₂(), P₁[ set ] } :

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

proof end;

scheme :: PARTFUN2:sch 3
UnPartFuncD{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> set , F₄( set ) -> Element of F₂() } :

for f, g being PartFunc of F₁(),F₂() st dom f = F₃() & ( for c being Element of F₁() st c in dom f holds
f /. c = F₄(c) ) & dom g = F₃() & ( for c being Element of F₁() st c in dom g holds
g /. c = F₄(c) ) holds
f = g

proof end;

definition

let C, D be non empty set ;
let SC be Subset of C;
let d be Element of D;
:: original: -->
redefine func SC --> d -> PartFunc of C,D;
coherence

proof end;

end;

theorem Th48: :: PARTFUN2:48

for C, D being non empty set
for SC being Subset of C
for c being Element of C
for d being Element of D st c in SC holds
(SC --> d) /. c = d

proof end;

theorem :: PARTFUN2:49

for D, C being non empty set
for d being Element of D
for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds
f /. c = d ) holds
f = (dom f) --> d

proof end;

theorem :: PARTFUN2:50

for E, C, D being non empty set
for SE being Subset of E
for c being Element of C
for f being PartFunc of C,D st c in dom f holds
f * (SE --> c) = SE --> (f /. c)

proof end;

theorem :: PARTFUN2:51

for C being non empty set
for SC being Subset of C holds
( id SC is total iff SC = C )

proof end;

theorem :: PARTFUN2:52

for C, D being non empty set
for SC being Subset of C
for d being Element of D st SC --> d is total holds
SC <> {}

proof end;

theorem :: PARTFUN2:53

for D, C being non empty set
for SC being Subset of C
for d being Element of D holds
( SC --> d is total iff SC = C )

proof end;

definition

let C, D be non empty set ;
let f be PartFunc of C,D;
let X be set ;
canceled;
canceled;
pred f is_constant_on X means :Def3: :: PARTFUN2:def 3
ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d;

end;

:: deftheorem PARTFUN2:def 1 :

:: deftheorem PARTFUN2:def 2 :

:: deftheorem Def3 defines is_constant_on PARTFUN2:def 3 :

theorem :: PARTFUN2:54

canceled;

theorem :: PARTFUN2:55

for X being set
for D, C being non empty set
for f being PartFunc of C,D holds
( f is_constant_on X iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f /. c1 = f /. c2 )

proof end;

theorem :: PARTFUN2:56

for X being set
for C, D being non empty set
for f being PartFunc of C,D st X meets dom f holds
( f is_constant_on X iff ex d being Element of D st rng (f | X) = {d} )

proof end;

theorem :: PARTFUN2:57

for X, Y being set
for C, D being non empty set
for f being PartFunc of C,D st f is_constant_on X & Y c= X holds
f is_constant_on Y

proof end;

theorem Th58: :: PARTFUN2:58

for X being set
for C, D being non empty set
for f being PartFunc of C,D st X misses dom f holds
f is_constant_on X

proof end;

theorem :: PARTFUN2:59

for C, D being non empty set
for SC being Subset of C
for d being Element of D
for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds
f is_constant_on SC

proof end;

theorem :: PARTFUN2:60

for x being set
for C, D being non empty set
for f being PartFunc of C,D holds f is_constant_on {x}

proof end;

theorem :: PARTFUN2:61

for X, Y being set
for C, D being non empty set
for f being PartFunc of C,D st f is_constant_on X & f is_constant_on Y & X /\ Y meets dom f holds
f is_constant_on X \/ Y

proof end;

theorem :: PARTFUN2:62

for Y, X being set
for C, D being non empty set
for f being PartFunc of C,D st f is_constant_on Y holds
f | X is_constant_on Y

proof end;

theorem :: PARTFUN2:63

for C, D being non empty set
for SC being Subset of C
for d being Element of D holds SC --> d is_constant_on SC

proof end;

theorem :: PARTFUN2:64

for D, C being non empty set
for f, g being PartFunc of C,D holds
( f c= g iff ( dom f c= dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) ) )

proof end;

theorem Th65: :: PARTFUN2:65

for C, D being non empty set
for c being Element of C
for d being Element of D
for f being PartFunc of C,D holds
( ( c in dom f & d = f /. c ) iff [c,d] in f )

proof end;

theorem :: PARTFUN2:66

for C, D, E being non empty set
for c being Element of C
for e being Element of E
for f being PartFunc of C,D
for s being PartFunc of D,E st [c,e] in s * f holds
( [c,(f /. c)] in f & [(f /. c),e] in s )

proof end;

theorem :: PARTFUN2:67

for C, D being non empty set
for c being Element of C
for d being Element of D
for f being PartFunc of C,D st f = {[c,d]} holds
f /. c = d

proof end;

theorem :: PARTFUN2:68

for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st dom f = {c} holds
f = {[c,(f /. c)]}

proof end;

theorem :: PARTFUN2:69

for C, D being non empty set
for c being Element of C
for f1, f, g being PartFunc of C,D st f1 = f /\ g & c in dom f1 holds
( f1 /. c = f /. c & f1 /. c = g /. c )

proof end;

theorem :: PARTFUN2:70

for C, D being non empty set
for c being Element of C
for f, f1, g being PartFunc of C,D st c in dom f & f1 = f \/ g holds
f1 /. c = f /. c

proof end;

theorem :: PARTFUN2:71

for C, D being non empty set
for c being Element of C
for g, f1, f being PartFunc of C,D st c in dom g & f1 = f \/ g holds
f1 /. c = g /. c

proof end;

theorem :: PARTFUN2:72

for C, D being non empty set
for c being Element of C
for f1, f, g being PartFunc of C,D st c in dom f1 & f1 = f \/ g & not f1 /. c = f /. c holds
f1 /. c = g /. c

proof end;

theorem :: PARTFUN2:73

for C, D being non empty set
for SC being Subset of C
for c being Element of C
for f being PartFunc of C,D holds
( ( c in dom f & c in SC ) iff [c,(f /. c)] in f | SC )

proof end;

theorem :: PARTFUN2:74

for C, D being non empty set
for SD being Subset of D
for c being Element of C
for f being PartFunc of C,D holds
( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD | f )

proof end;

theorem :: PARTFUN2:75

for C, D being non empty set
for SD being Subset of D
for c being Element of C
for f being PartFunc of C,D holds
( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )

proof end;

theorem Th76: :: PARTFUN2:76

for X being set
for D, C being non empty set
for f being PartFunc of C,D holds
( f is_constant_on X iff ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f . c = d )

proof end;

theorem :: PARTFUN2:77

for X being set
for D, C being non empty set
for f being PartFunc of C,D holds
( f is_constant_on X iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2 )

proof end;

theorem :: PARTFUN2:78

for X being set
for D, C being non empty set
for d being Element of D
for f being PartFunc of C,D st d in f .: X holds
ex c being Element of C st
( c in dom f & c in X & d = f . c )

proof end;

theorem :: PARTFUN2:79

for C, D being non empty set
for c being Element of C
for d being Element of D
for f being PartFunc of C,D st f is one-to-one holds
( d in rng f & c = (f " ) . d iff ( c in dom f & d = f . c ) )

proof end;