:: Partial Functions from a Domain to a Domain
:: by Jaros{\l}aw Kotowicz
::
:: Received May 31, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem Th1: :: PARTFUN2:1
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 Th2: :: PARTFUN2:2
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 Th3: :: PARTFUN2:3
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 Th4: :: PARTFUN2:4
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:5
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
id SD is PartFunc of D,D
proof end;
end;

theorem Th6: :: PARTFUN2:6
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:7
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:8
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:9
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:10
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;

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
f " is PartFunc of Y,X by PARTFUN1:9;
end;

theorem Th11: :: PARTFUN2:11
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:12
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:13
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:14
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 Th15: :: PARTFUN2:15
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 Th16: :: PARTFUN2:16
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:17
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:18
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
X |` f is PartFunc of C,D by PARTFUN1:13;
end;

theorem Th19: :: PARTFUN2:19
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:20
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 Th19;

theorem :: PARTFUN2:21
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 Th19;

theorem Th22: :: PARTFUN2:22
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:23
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 Th22;

theorem :: PARTFUN2:24
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
Im (f,c) = {(f /. c)}
proof end;

theorem :: PARTFUN2:25
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 Th26: :: PARTFUN2:26
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:27
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:28
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{ F1() -> non empty set , F2() -> non empty set , P1[ set , set ] } :
ex f being PartFunc of F1(),F2() st
( ( for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st P1[d,c] ) ) & ( for d being Element of F1() st d in dom f holds
P1[d,f /. d] ) )
proof end;

scheme :: PARTFUN2:sch 2
LambdaPFD{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> Element of F2(), P1[ set ] } :
ex f being PartFunc of F1(),F2() st
( ( for d being Element of F1() holds
( d in dom f iff P1[d] ) ) & ( for d being Element of F1() st d in dom f holds
f /. d = F3(d) ) )
proof end;

scheme :: PARTFUN2:sch 3
UnPartFuncD{ F1() -> non empty set , F2() -> non empty set , F3() -> set , F4( set ) -> Element of F2() } :
for f, g being PartFunc of F1(),F2() st dom f = F3() & ( for c being Element of F1() st c in dom f holds
f /. c = F4(c) ) & dom g = F3() & ( for c being Element of F1() st c in dom g holds
g /. c = F4(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
SC --> d is PartFunc of C,D
proof end;
end;

theorem Th29: :: PARTFUN2:29
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:30
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:31
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:32
for C being non empty set
for SC being Subset of C holds
( id SC is total iff SC = C )
proof end;

theorem :: PARTFUN2:33
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:34
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;

::
:: PARTIAL FUNCTION CONSTANT ON SET
::
definition
let C, D be non empty set ;
let f be PartFunc of C,D;
:: original: constant
redefine attr f is constant means :: PARTFUN2:def 1
 ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d;
compatibility
( f is constant iff ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d )
proof end;
end;

:: deftheorem defines constant PARTFUN2:def 1 :
for C, D being non empty set
for f being PartFunc of C,D holds
( f is constant iff ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d );

theorem Th35: :: PARTFUN2:35
for X being set
for D, C being non empty set
for f being PartFunc of C,D holds
( f | X is V8() 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:36
for X being set
for D, C being non empty set
for f being PartFunc of C,D holds
( f | X is V8() 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:37
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 | X is V8() iff ex d being Element of D st rng (f | X) = {d} )
proof end;

theorem :: PARTFUN2:38
for X, Y being set
for C, D being non empty set
for f being PartFunc of C,D st f | X is V8() & Y c= X holds
f | Y is V8()
proof end;

theorem Th39: :: PARTFUN2:39
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 | X is V8()
proof end;

theorem :: PARTFUN2:40
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 | SC is V8()
proof end;

theorem :: PARTFUN2:41
for x being set
for C, D being non empty set
for f being PartFunc of C,D holds f | {x} is V8()
proof end;

theorem :: PARTFUN2:42
for X, Y being set
for C, D being non empty set
for f being PartFunc of C,D st f | X is V8() & f | Y is V8() & X /\ Y meets dom f holds
f | (X \/ Y) is V8()
proof end;

theorem :: PARTFUN2:43
for Y, X being set
for C, D being non empty set
for f being PartFunc of C,D st f | Y is V8() holds
(f | X) | Y is V8()
proof end;

theorem :: PARTFUN2:44
for C, D being non empty set
for SC being Subset of C
for d being Element of D holds (SC --> d) | SC is V8()
proof end;

::
:: OF PARTIAL FUNCTION FROM A DOMAIN TO A DOMAIN
::
theorem :: PARTFUN2:45
for D, C being non empty set
for f, g being PartFunc of C,D st dom f c= dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) holds
f c= g
proof end;

theorem Th46: :: PARTFUN2:46
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:47
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:48
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:49
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:50
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:51
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:52
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:53
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:54
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:55
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:56
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 Th57: :: PARTFUN2:57
for X being set
for D, C being non empty set
for f being PartFunc of C,D holds
( f | X is V8() 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:58
for X being set
for D, C being non empty set
for f being PartFunc of C,D holds
( f | X is V8() 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:59
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:60
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;

theorem :: PARTFUN2:61
for Y being set
for f, g being b1 -valued Function st f c= g holds
for x being set st x in dom f holds
f /. x = g /. x
proof end;