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

theorem Th1: :: PARTFUN2:1

for C, D 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 C, D 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 C, D, E 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 C, D 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 C, D being non empty set
for f, g 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 C, D being non empty set
for f, g 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 C, D 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 C, D 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 C, D 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 C, D 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₁[ object , object ] } :

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
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 C, D 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 C, D, E 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 C, D 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 C, D 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 C, D 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 X, Y 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 C, D 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 f, f1, 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 f, f1, g 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 f, f1, 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 C, D 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 C, D 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 C, D 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 b₁ -valued Function st f c= g holds
for x being set st x in dom f holds
f /. x = g /. x

proof end;