:: by Czes{\l}aw Byli\'nski

::

:: Received September 18, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

:: Auxiliary theorems

theorem Th1: :: PARTFUN1:1

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

f . x = g . x ) holds

ex h being Function st f \/ g = h

proof end;

theorem Th2: :: PARTFUN1:2

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

for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x

proof end;

Lm1: now :: thesis: for X, Y being set ex E being set st

( dom E c= X & rng E c= Y )

( 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 ) by XBOOLE_1:2; :: thesis: verum

end;
( 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 ) by XBOOLE_1:2; :: thesis: verum

registration
end;

theorem :: PARTFUN1:3

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 )

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

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;

scheme :: PARTFUN1:sch 2

PartFuncEx{ F_{1}() -> set , F_{2}() -> set , P_{1}[ set , set ] } :

PartFuncEx{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for x being set holds

( x in dom f iff ( x in F_{1}() & ex y being set st P_{1}[x,y] ) ) ) & ( for x being set st x in dom f holds

P_{1}[x,f . x] ) )

provided( ( for x being set holds

( x in dom f iff ( x in F

P

A1:
for x, y being set st x in F_{1}() & P_{1}[x,y] holds

y in F_{2}()
and

A2: for x, y1, y2 being set st x in F_{1}() & P_{1}[x,y1] & P_{1}[x,y2] holds

y1 = y2

y in F

A2: for x, y1, y2 being set st x in F

y1 = y2

proof end;

scheme :: PARTFUN1:sch 3

LambdaR{ F_{1}() -> set , F_{2}() -> set , F_{3}( set ) -> set , P_{1}[ set ] } :

LambdaR{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for x being set holds

( x in dom f iff ( x in F_{1}() & P_{1}[x] ) ) ) & ( for x being set st x in dom f holds

f . x = F_{3}(x) ) )

provided
( ( for x being set holds

( x in dom f iff ( x in F

f . x = 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

end;
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;

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

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;

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

theorem :: PARTFUN1:13

theorem :: PARTFUN1:15

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 )

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

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

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

:: Construction of a Partial Function from a Function

definition
end;

:: deftheorem defines <: PARTFUN1:def 1 :

for f being Function

for X, Y being set holds <:f,X,Y:> = (Y |` f) | X;

for f being Function

for X, Y being set holds <:f,X,Y:> = (Y |` f) | X;

theorem Th24: :: PARTFUN1:24

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

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

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

for f being Function st X1 c= X2 & Y1 c= Y2 holds

<:f,X1,Y1:> c= <:f,X2,Y2:>

proof end;

theorem :: PARTFUN1:36

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

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;

:: Total Function

:: deftheorem Def2 defines total PARTFUN1:def 2 :

for X being set

for f being b_{1} -defined Relation holds

( f is total iff dom f = X );

for X being set

for f being b

( f is total iff dom f = X );

registration

let X be empty set ;

let Y be set ;

coherence

for b_{1} being Relation of X,Y holds b_{1} is total

end;
let Y be set ;

coherence

for b

proof end;

registration

let X be non empty set ;

let Y be empty set ;

coherence

for b_{1} being Relation of X,Y holds not b_{1} is total

end;
let Y be empty set ;

coherence

for b

proof end;

:: set of partial functions from a set into a set

definition

let X, Y be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex f being Function st

( x = f & dom f c= X & rng f c= Y ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex f being Function st

( x = f & dom f c= X & rng f c= Y ) ) ) & ( for x being set holds

( x in b_{2} iff ex f being Function st

( x = f & dom f c= X & rng f c= Y ) ) ) holds

b_{1} = b_{2}

end;
func PFuncs (X,Y) -> set means :Def3: :: PARTFUN1:def 3

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 for x being set holds

( x in it iff ex f being Function st

( x = f & dom f c= X & rng f c= Y ) );

ex b

for x being set holds

( x in b

( x = f & dom f c= X & rng f c= Y ) )

proof end;

uniqueness for b

( x in b

( x = f & dom f c= X & rng f c= Y ) ) ) & ( for x being set holds

( x in b

( x = f & dom f c= X & rng f c= Y ) ) ) holds

b

proof end;

:: deftheorem Def3 defines PFuncs PARTFUN1:def 3 :

for X, Y, b_{3} being set holds

( b_{3} = PFuncs (X,Y) iff for x being set holds

( x in b_{3} iff ex f being Function st

( x = f & dom f c= X & rng f c= Y ) ) );

for X, Y, b

( b

( x in b

( x = f & dom f c= X & rng f c= Y ) ) );

theorem :: PARTFUN1:47

:: Relation of Tolerance on Functions

definition

let f, g be Function;

for f being Function

for x being set st x in (dom f) /\ (dom f) holds

f . x = f . x ;

symmetry

for f, g being Function st ( for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x ) holds

for x being set st x in (dom g) /\ (dom f) holds

g . x = f . x ;

end;
pred f tolerates g means :Def4: :: PARTFUN1:def 4

for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x;

reflexivity for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x;

for f being Function

for x being set st x in (dom f) /\ (dom f) holds

f . x = f . x ;

symmetry

for f, g being Function st ( for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x ) holds

for x being set st x in (dom g) /\ (dom f) holds

g . x = f . x ;

:: deftheorem Def4 defines tolerates PARTFUN1:def 4 :

for f, g being Function holds

( f tolerates g iff for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x );

for f, g being Function holds

( f tolerates g iff for x being set st x in (dom f) /\ (dom g) holds

f . x = g . x );

theorem Th53: :: PARTFUN1:53

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 )

( f tolerates g iff for x being set st x in dom f holds

f . x = g . x )

proof end;

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

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

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

f = g

proof end;

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

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 )

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;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex g being PartFunc of X,Y st

( g = x & g is total & f tolerates g ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex g being PartFunc of X,Y st

( g = x & g is total & f tolerates g ) ) ) & ( for x being set holds

( x in b_{2} iff ex g being PartFunc of X,Y st

( g = x & g is total & f tolerates g ) ) ) holds

b_{1} = b_{2}

end;
let f be PartFunc of X,Y;

func TotFuncs f -> set means :Def5: :: PARTFUN1:def 5

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

ex b

for x being set holds

( x in b

( g = x & g is total & f tolerates g ) )

proof end;

uniqueness for b

( x in b

( g = x & g is total & f tolerates g ) ) ) & ( for x being set holds

( x in b

( g = x & g is total & f tolerates g ) ) ) holds

b

proof end;

:: deftheorem Def5 defines TotFuncs PARTFUN1:def 5 :

for X, Y being set

for f being PartFunc of X,Y

for b_{4} being set holds

( b_{4} = TotFuncs f iff for x being set holds

( x in b_{4} iff ex g being PartFunc of X,Y st

( g = x & g is total & f tolerates g ) ) );

for X, Y being set

for f being PartFunc of X,Y

for b

( b

( x in b

( 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

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

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;

coherence

TotFuncs f is empty

end;
let Y be empty set ;

let f be PartFunc of X,Y;

coherence

TotFuncs f is empty

proof end;

theorem :: PARTFUN1:74

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

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

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

TotFuncs f meets TotFuncs g

proof end;

begin

Lm2: for X being set

for R being Relation of X st R = id X holds

R is total

proof end;

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 ;

ex b_{1} being Relation of X st

( b_{1} is total & b_{1} is reflexive & b_{1} is symmetric & b_{1} is antisymmetric & b_{1} is transitive )

end;
cluster Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive total for Element of bool [:X,X:];

existence ex b

( b

proof end;

registration

coherence

for b_{1} being Relation st b_{1} is symmetric & b_{1} is transitive holds

b_{1} is reflexive

end;
for b

b

proof end;

registration
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;
:: original: id

redefine func id X -> total Relation of X;

coherence

id X is total Relation of X by Lm2, Lm4;

begin

theorem Th77: :: PARTFUN1:77

for x, y, z being set

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

y = z

for f, g being Function 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

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 set ;

assume A1: i in dom p ;

coherence

p . i is Element of D by A1, Th4;

end;
let p be D -valued Function;

let i be set ;

assume A1: i in dom p ;

coherence

p . i is Element of D by A1, Th4;

:: deftheorem Def6 defines /. PARTFUN1:def 6 :

for D being set

for p being b_{1} -valued Function

for i being set st i in dom p holds

p /. i = p . i;

for D being set

for p being b

for i being set st i in dom p holds

p /. i = p . i;

:: missing, 2008.09.15, A.T.

registration

let X, Y be non empty set ;

existence

not for b_{1} being PartFunc of X,Y holds b_{1} is empty

end;
existence

not for b

proof end;

:: from FRAENKEL, 2009.05.06, A.K.

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

f1 * g = f2 * g

proof end;

:: missing, 2011.06.06, A.T.

theorem :: PARTFUN1:80

for Y, x, X being set

for f being b_{1} -valued Function st x in dom (f | X) holds

(f | X) /. x = f /. x

for f being b

(f | X) /. x = f /. x

proof end;