:: FUNCT_1 semantic presentation

definition

let X be set ;
attr X is Function-like means :Def1: :: FUNCT_1:def 1
for x, y1, y2 being set st [x,y1] in X & [x,y2] in X holds
y1 = y2;

end;

:: deftheorem Def1 defines Function-like FUNCT_1:def 1 :

registration

cluster Relation-like Function-like set ;
existence

proof end;

end;

definition

mode Function is Relation-like Function-like set ;

end;

registration

cluster empty -> Function-like set ;
coherence

proof end;

end;

theorem :: FUNCT_1:1

canceled;

theorem :: FUNCT_1:2

for F being set st ( for p being set st p in F holds
ex x, y being set st [x,y] = p ) & ( for x, y1, y2 being set st [x,y1] in F & [x,y2] in F holds
y1 = y2 ) holds
F is Function by Def1, RELAT_1:def 1;

scheme :: FUNCT_1:sch 1
GraphFunc{ F₁() -> set , P₁[ set , set ] } :

ex f being Function st
for x, y being set holds
( [x,y] in f iff ( x in F₁() & P₁[x,y] ) )

provided

A1: for x, y1, y2 being set st P₁[x,y1] & P₁[x,y2] holds
y1 = y2

proof end;

definition

let f be Function;
let x be set ;
canceled;
canceled;
func f . x -> set means :Def4: :: FUNCT_1:def 4
[x,it] in f if x in dom f
otherwise it = {} ;
existence by RELAT_1:def 4;
uniqueness by Def1;
consistency ;

end;

:: deftheorem FUNCT_1:def 2 :

:: deftheorem FUNCT_1:def 3 :

:: deftheorem Def4 defines . FUNCT_1:def 4 :

theorem :: FUNCT_1:3

canceled;

theorem :: FUNCT_1:4

canceled;

theorem :: FUNCT_1:5

canceled;

theorem :: FUNCT_1:6

canceled;

theorem :: FUNCT_1:7

canceled;

theorem Th8: :: FUNCT_1:8

for x, y being set
for f being Function holds
( [x,y] in f iff ( x in dom f & y = f . x ) )

proof end;

theorem Th9: :: FUNCT_1:9

for f, g being Function st dom f = dom g & ( for x being set st x in dom f holds
f . x = g . x ) holds
f = g

proof end;

definition

let f be Function;
redefine func rng f means :Def5: :: FUNCT_1:def 5
for y being set holds
( y in it iff ex x being set st
( x in dom f & y = f . x ) );
compatibility

proof end;

end;

:: deftheorem Def5 defines rng FUNCT_1:def 5 :

theorem :: FUNCT_1:10

canceled;

theorem :: FUNCT_1:11

canceled;

theorem :: FUNCT_1:12

for x being set
for f being Function st x in dom f holds
f . x in rng f by Def5;

theorem :: FUNCT_1:13

canceled;

theorem Th14: :: FUNCT_1:14

for x being set
for f being Function st dom f = {x} holds
rng f = {(f . x)}

proof end;

scheme :: FUNCT_1:sch 2
FuncEx{ F₁() -> set , P₁[ set , set ] } :

ex f being Function st
( dom f = F₁() & ( for x being set st x in F₁() holds
P₁[x,f . x] ) )

provided

A1: for x, y1, y2 being set st x in F₁() & P₁[x,y1] & P₁[x,y2] holds
y1 = y2 and
A2: for x being set st x in F₁() holds
ex y being set st P₁[x,y]

proof end;

scheme :: FUNCT_1:sch 3
Lambda{ F₁() -> set , F₂( set ) -> set } :

ex f being Function st
( dom f = F₁() & ( for x being set st x in F₁() holds
f . x = F₂(x) ) )

proof end;

theorem :: FUNCT_1:15

for X being set st X <> {} holds
for y being set ex f being Function st
( dom f = X & rng f = {y} )

proof end;

theorem :: FUNCT_1:16

for X being set st ( for f, g being Function st dom f = X & dom g = X holds
f = g ) holds
X = {}

proof end;

theorem :: FUNCT_1:17

for y being set
for f, g being Function st dom f = dom g & rng f = {y} & rng g = {y} holds
f = g

proof end;

theorem :: FUNCT_1:18

for Y, X being set st ( Y <> {} or X = {} ) holds
ex f being Function st
( X = dom f & rng f c= Y )

proof end;

theorem :: FUNCT_1:19

for Y being set
for f being Function st ( for y being set st y in Y holds
ex x being set st
( x in dom f & y = f . x ) ) holds
Y c= rng f

proof end;

notation

let f, g be Function;
synonym g * f for f * g;

end;

registration

let f, g be Function;
cluster g * f -> Function-like ;
coherence

proof end;

end;

theorem :: FUNCT_1:20

for f, g, h being Function st ( for x being set holds
( x in dom h iff ( x in dom f & f . x in dom g ) ) ) & ( for x being set st x in dom h holds
h . x = g . (f . x) ) holds
h = g * f

proof end;

theorem Th21: :: FUNCT_1:21

for x being set
for g, f being Function holds
( x in dom (g * f) iff ( x in dom f & f . x in dom g ) )

proof end;

theorem Th22: :: FUNCT_1:22

for x being set
for g, f being Function st x in dom (g * f) holds
(g * f) . x = g . (f . x)

proof end;

theorem Th23: :: FUNCT_1:23

for x being set
for f, g being Function st x in dom f holds
(g * f) . x = g . (f . x)

proof end;

theorem :: FUNCT_1:24

canceled;

theorem :: FUNCT_1:25

for z being set
for g, f being Function st z in rng (g * f) holds
z in rng g

proof end;

theorem :: FUNCT_1:26

canceled;

theorem Th27: :: FUNCT_1:27

for g, f being Function st dom (g * f) = dom f holds
rng f c= dom g

proof end;

theorem :: FUNCT_1:28

canceled;

theorem :: FUNCT_1:29

canceled;

theorem :: FUNCT_1:30

canceled;

theorem :: FUNCT_1:31

canceled;

theorem :: FUNCT_1:32

canceled;

theorem :: FUNCT_1:33

for Y being set
for f being Function st rng f c= Y & ( for g, h being Function st dom g = Y & dom h = Y & g * f = h * f holds
g = h ) holds
Y = rng f

proof end;

registration

let X be set ;
cluster id X -> Function-like ;
coherence

proof end;

end;

theorem Th34: :: FUNCT_1:34

for X being set
for f being Function holds
( f = id X iff ( dom f = X & ( for x being set st x in X holds
f . x = x ) ) )

proof end;

theorem :: FUNCT_1:35

for X, x being set st x in X holds
(id X) . x = x by Th34;

theorem :: FUNCT_1:36

canceled;

theorem Th37: :: FUNCT_1:37

for X being set
for f being Function holds dom (f * (id X)) = (dom f) /\ X

proof end;

theorem :: FUNCT_1:38

for X, x being set
for f being Function st x in (dom f) /\ X holds
f . x = (f * (id X)) . x

proof end;

theorem :: FUNCT_1:39

canceled;

theorem :: FUNCT_1:40

for Y, x being set
for f being Function holds
( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) )

proof end;

theorem :: FUNCT_1:41

canceled;

theorem :: FUNCT_1:42

for f being Function holds
( f * (id (dom f)) = f & (id (rng f)) * f = f ) by RELAT_1:77, RELAT_1:79;

theorem :: FUNCT_1:43

for X, Y being set holds (id X) * (id Y) = id (X /\ Y)

proof end;

theorem Th44: :: FUNCT_1:44

for f, g being Function st rng f = dom g & g * f = f holds
g = id (dom g)

proof end;

definition

let f be Function;
canceled;
canceled;
attr f is one-to-one means :Def8: :: FUNCT_1:def 8
for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2;

end;

:: deftheorem FUNCT_1:def 6 :

:: deftheorem FUNCT_1:def 7 :

:: deftheorem Def8 defines one-to-one FUNCT_1:def 8 :

theorem :: FUNCT_1:45

canceled;

theorem Th46: :: FUNCT_1:46

for f, g being Function st f is one-to-one & g is one-to-one holds
g * f is one-to-one

proof end;

theorem Th47: :: FUNCT_1:47

for g, f being Function st g * f is one-to-one & rng f c= dom g holds
f is one-to-one

proof end;

theorem :: FUNCT_1:48

for g, f being Function st g * f is one-to-one & rng f = dom g holds
( f is one-to-one & g is one-to-one )

proof end;

theorem :: FUNCT_1:49

for f being Function holds
( f is one-to-one iff for g, h being Function st rng g c= dom f & rng h c= dom f & dom g = dom h & f * g = f * h holds
g = h )

proof end;

theorem :: FUNCT_1:50

for X being set
for f, g being Function st dom f = X & dom g = X & rng g c= X & f is one-to-one & f * g = f holds
g = id X

proof end;

theorem :: FUNCT_1:51

for g, f being Function st rng (g * f) = rng g & g is one-to-one holds
dom g c= rng f

proof end;

theorem Th52: :: FUNCT_1:52

for X being set holds id X is one-to-one

proof end;

theorem :: FUNCT_1:53

for f being Function st ex g being Function st g * f = id (dom f) holds
f is one-to-one

proof end;

registration

cluster empty set ;
existence

proof end;

end;

registration

cluster empty -> one-to-one set ;
coherence

proof end;

end;

registration

cluster one-to-one set ;
existence

proof end;

end;

registration

let f be one-to-one Function;
cluster f ~ -> Function-like ;
coherence

proof end;

end;

definition

let f be Function;
assume A1: f is one-to-one ;
func f " -> Function equals :Def9: :: FUNCT_1:def 9
f ~ ;
coherence

proof end;

end;

:: deftheorem Def9 defines " FUNCT_1:def 9 :

theorem Th54: :: FUNCT_1:54

for f being Function st f is one-to-one holds
for g being Function holds
( g = f " iff ( dom g = rng f & ( for y, x being set holds
( y in rng f & x = g . y iff ( x in dom f & y = f . x ) ) ) ) )

proof end;

theorem Th55: :: FUNCT_1:55

for f being Function st f is one-to-one holds
( rng f = dom (f " ) & dom f = rng (f " ) )

proof end;

theorem Th56: :: FUNCT_1:56

for x being set
for f being Function st f is one-to-one & x in dom f holds
( x = (f " ) . (f . x) & x = ((f " ) * f) . x )

proof end;

theorem Th57: :: FUNCT_1:57

for y being set
for f being Function st f is one-to-one & y in rng f holds
( y = f . ((f " ) . y) & y = (f * (f " )) . y )

proof end;

theorem Th58: :: FUNCT_1:58

for f being Function st f is one-to-one holds
( dom ((f " ) * f) = dom f & rng ((f " ) * f) = dom f )

proof end;

theorem Th59: :: FUNCT_1:59

for f being Function st f is one-to-one holds
( dom (f * (f " )) = rng f & rng (f * (f " )) = rng f )

proof end;

theorem :: FUNCT_1:60

for f, g being Function st f is one-to-one & dom f = rng g & rng f = dom g & ( for x, y being set st x in dom f & y in dom g holds
( f . x = y iff g . y = x ) ) holds
g = f "

proof end;

theorem Th61: :: FUNCT_1:61

for f being Function st f is one-to-one holds
( (f " ) * f = id (dom f) & f * (f " ) = id (rng f) )

proof end;

theorem Th62: :: FUNCT_1:62

for f being Function st f is one-to-one holds
f " is one-to-one

proof end;

Lm1: for X being set
for g2, f, g1 being Function st rng g2 = X & f * g2 = id (dom g1) & g1 * f = id X holds
g1 = g2

proof end;

theorem Th63: :: FUNCT_1:63

for f, g being Function st f is one-to-one & rng f = dom g & g * f = id (dom f) holds
g = f "

proof end;

theorem :: FUNCT_1:64

for f, g being Function st f is one-to-one & rng g = dom f & f * g = id (rng f) holds
g = f "

proof end;

theorem :: FUNCT_1:65

for f being Function st f is one-to-one holds
(f " ) " = f

proof end;

theorem :: FUNCT_1:66

for f, g being Function st f is one-to-one & g is one-to-one holds
(g * f) " = (f " ) * (g " )

proof end;

theorem :: FUNCT_1:67

for X being set holds (id X) " = id X

proof end;

registration

let f be Function;
let X be set ;
cluster f | X -> Function-like ;
coherence

proof end;

end;

theorem Th68: :: FUNCT_1:68

for X being set
for g, f being Function holds
( g = f | X iff ( dom g = (dom f) /\ X & ( for x being set st x in dom g holds
g . x = f . x ) ) )

proof end;

theorem :: FUNCT_1:69

canceled;

theorem :: FUNCT_1:70

for X, x being set
for f being Function st x in dom (f | X) holds
(f | X) . x = f . x by Th68;

theorem :: FUNCT_1:71

for X, x being set
for f being Function st x in (dom f) /\ X holds
(f | X) . x = f . x

proof end;

Lm2: for X, x being set
for f being Function holds
( x in dom (f | X) iff ( x in dom f & x in X ) )

proof end;

theorem Th72: :: FUNCT_1:72

for X, x being set
for f being Function st x in X holds
(f | X) . x = f . x

proof end;

theorem :: FUNCT_1:73

for X, x being set
for f being Function st x in dom f & x in X holds
f . x in rng (f | X)

proof end;

theorem :: FUNCT_1:74

canceled;

theorem :: FUNCT_1:75

canceled;

theorem :: FUNCT_1:76

for X being set
for f being Function holds
( dom (f | X) c= dom f & rng (f | X) c= rng f ) by RELAT_1:89, RELAT_1:99;

theorem :: FUNCT_1:77

canceled;

theorem :: FUNCT_1:78

canceled;

theorem :: FUNCT_1:79

canceled;

theorem :: FUNCT_1:80

canceled;

theorem :: FUNCT_1:81

canceled;

theorem :: FUNCT_1:82

for X, Y being set
for f being Function st X c= Y holds
( (f | X) | Y = f | X & (f | Y) | X = f | X ) by RELAT_1:102, RELAT_1:103;

theorem :: FUNCT_1:83

canceled;

theorem :: FUNCT_1:84

for X being set
for f being Function st f is one-to-one holds
f | X is one-to-one

proof end;

registration

let Y be set ;
let f be Function;
cluster Y | f -> Function-like ;
coherence

proof end;

end;

theorem Th85: :: FUNCT_1:85

for Y being set
for g, f being Function holds
( g = Y | f iff ( ( for x being set holds
( x in dom g iff ( x in dom f & f . x in Y ) ) ) & ( for x being set st x in dom g holds
g . x = f . x ) ) )

proof end;

theorem :: FUNCT_1:86

for Y, x being set
for f being Function holds
( x in dom (Y | f) iff ( x in dom f & f . x in Y ) ) by Th85;

theorem :: FUNCT_1:87

for Y, x being set
for f being Function st x in dom (Y | f) holds
(Y | f) . x = f . x by Th85;

theorem :: FUNCT_1:88

canceled;

theorem :: FUNCT_1:89

for Y being set
for f being Function holds
( dom (Y | f) c= dom f & rng (Y | f) c= rng f )

proof end;

theorem :: FUNCT_1:90

canceled;

theorem :: FUNCT_1:91

canceled;

theorem :: FUNCT_1:92

canceled;

theorem :: FUNCT_1:93

canceled;

theorem :: FUNCT_1:94

canceled;

theorem :: FUNCT_1:95

canceled;

theorem :: FUNCT_1:96

canceled;

theorem :: FUNCT_1:97

for X, Y being set
for f being Function st X c= Y holds
( Y | (X | f) = X | f & X | (Y | f) = X | f ) by RELAT_1:129, RELAT_1:130;

theorem :: FUNCT_1:98

canceled;

theorem :: FUNCT_1:99

for Y being set
for f being Function st f is one-to-one holds
Y | f is one-to-one

proof end;

definition

let f be Function;
let X be set ;
canceled;
canceled;
redefine func f .: X means :Def12: :: FUNCT_1:def 12
for y being set holds
( y in it iff ex x being set st
( x in dom f & x in X & y = f . x ) );
compatibility

proof end;

end;

:: deftheorem FUNCT_1:def 10 :

:: deftheorem FUNCT_1:def 11 :

:: deftheorem Def12 defines .: FUNCT_1:def 12 :

theorem :: FUNCT_1:100

canceled;

theorem :: FUNCT_1:101

canceled;

theorem :: FUNCT_1:102

canceled;

theorem :: FUNCT_1:103

canceled;

theorem :: FUNCT_1:104

canceled;

theorem :: FUNCT_1:105

canceled;

theorem :: FUNCT_1:106

canceled;

theorem :: FUNCT_1:107

canceled;

theorem :: FUNCT_1:108

canceled;

theorem :: FUNCT_1:109

canceled;

theorem :: FUNCT_1:110

canceled;

theorem :: FUNCT_1:111

canceled;

theorem :: FUNCT_1:112

canceled;

theorem :: FUNCT_1:113

canceled;

theorem :: FUNCT_1:114

canceled;

theorem :: FUNCT_1:115

canceled;

theorem :: FUNCT_1:116

canceled;

theorem Th117: :: FUNCT_1:117

for x being set
for f being Function st x in dom f holds
f .: {x} = {(f . x)}

proof end;

theorem :: FUNCT_1:118

for x1, x2 being set
for f being Function st x1 in dom f & x2 in dom f holds
f .: {x1,x2} = {(f . x1),(f . x2)}

proof end;

theorem :: FUNCT_1:119

canceled;

theorem :: FUNCT_1:120

for Y, X being set
for f being Function holds (Y | f) .: X c= f .: X

proof end;

theorem Th121: :: FUNCT_1:121

for X1, X2 being set
for f being Function st f is one-to-one holds
f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2)

proof end;

theorem :: FUNCT_1:122

for f being Function st ( for X1, X2 being set holds f .: (X1 /\ X2) = (f .: X1) /\ (f .: X2) ) holds
f is one-to-one

proof end;

theorem :: FUNCT_1:123

for X1, X2 being set
for f being Function st f is one-to-one holds
f .: (X1 \ X2) = (f .: X1) \ (f .: X2)

proof end;

theorem :: FUNCT_1:124

for f being Function st ( for X1, X2 being set holds f .: (X1 \ X2) = (f .: X1) \ (f .: X2) ) holds
f is one-to-one

proof end;

theorem :: FUNCT_1:125

for X, Y being set
for f being Function st X misses Y & f is one-to-one holds
f .: X misses f .: Y

proof end;

theorem :: FUNCT_1:126

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

proof end;

definition

let f be Function;
let Y be set ;
redefine func f " Y means :Def13: :: FUNCT_1:def 13
for x being set holds
( x in it iff ( x in dom f & f . x in Y ) );
compatibility

proof end;

end;

:: deftheorem Def13 defines " FUNCT_1:def 13 :

theorem :: FUNCT_1:127

canceled;

theorem :: FUNCT_1:128

canceled;

theorem :: FUNCT_1:129

canceled;

theorem :: FUNCT_1:130

canceled;

theorem :: FUNCT_1:131

canceled;

theorem :: FUNCT_1:132

canceled;

theorem :: FUNCT_1:133

canceled;

theorem :: FUNCT_1:134

canceled;

theorem :: FUNCT_1:135

canceled;

theorem :: FUNCT_1:136

canceled;

theorem :: FUNCT_1:137

for Y1, Y2 being set
for f being Function holds f " (Y1 /\ Y2) = (f " Y1) /\ (f " Y2)

proof end;

theorem :: FUNCT_1:138

for Y1, Y2 being set
for f being Function holds f " (Y1 \ Y2) = (f " Y1) \ (f " Y2)

proof end;

theorem :: FUNCT_1:139

for X, Y being set
for R being Relation holds (R | X) " Y = X /\ (R " Y)

proof end;

theorem :: FUNCT_1:140

canceled;

theorem :: FUNCT_1:141

canceled;

theorem Th142: :: FUNCT_1:142

for y being set
for R being Relation holds
( y in rng R iff R " {y} <> {} )

proof end;

theorem :: FUNCT_1:143

for Y being set
for R being Relation st ( for y being set st y in Y holds
R " {y} <> {} ) holds
Y c= rng R

proof end;

theorem Th144: :: FUNCT_1:144

for f being Function holds
( ( for y being set st y in rng f holds
ex x being set st f " {y} = {x} ) iff f is one-to-one )

proof end;

theorem Th145: :: FUNCT_1:145

for Y being set
for f being Function holds f .: (f " Y) c= Y

proof end;

theorem :: FUNCT_1:146

for X being set
for R being Relation st X c= dom R holds
X c= R " (R .: X)

proof end;

theorem :: FUNCT_1:147

for Y being set
for f being Function st Y c= rng f holds
f .: (f " Y) = Y

proof end;

theorem :: FUNCT_1:148

for Y being set
for f being Function holds f .: (f " Y) = Y /\ (f .: (dom f))

proof end;

theorem Th149: :: FUNCT_1:149

for X, Y being set
for f being Function holds f .: (X /\ (f " Y)) c= (f .: X) /\ Y

proof end;

theorem :: FUNCT_1:150

for X, Y being set
for f being Function holds f .: (X /\ (f " Y)) = (f .: X) /\ Y

proof end;

theorem :: FUNCT_1:151

for X, Y being set
for R being Relation holds X /\ (R " Y) c= R " ((R .: X) /\ Y)

proof end;

theorem :: FUNCT_1:152

for X being set
for f being Function st f is one-to-one holds
f " (f .: X) c= X

proof end;

theorem :: FUNCT_1:153

for f being Function st ( for X being set holds f " (f .: X) c= X ) holds
f is one-to-one

proof end;

theorem :: FUNCT_1:154

for X being set
for f being Function st f is one-to-one holds
f .: X = (f " ) " X

proof end;

theorem :: FUNCT_1:155

for Y being set
for f being Function st f is one-to-one holds
f " Y = (f " ) .: Y

proof end;

theorem :: FUNCT_1:156

for Y being set
for f, g, h being Function st Y = rng f & dom g = Y & dom h = Y & g * f = h * f holds
g = h

proof end;

theorem :: FUNCT_1:157

for X1, X2 being set
for f being Function st f .: X1 c= f .: X2 & X1 c= dom f & f is one-to-one holds
X1 c= X2

proof end;

theorem Th158: :: FUNCT_1:158

for Y1, Y2 being set
for f being Function st f " Y1 c= f " Y2 & Y1 c= rng f holds
Y1 c= Y2

proof end;

theorem :: FUNCT_1:159

for f being Function holds
( f is one-to-one iff for y being set ex x being set st f " {y} c= {x} )

proof end;

theorem :: FUNCT_1:160

for X being set
for R, S being Relation st rng R c= dom S holds
R " X c= (R * S) " (S .: X)

proof end;

theorem :: FUNCT_1:161

for X, Y being set
for f being Function st f " X = f " Y & X c= rng f & Y c= rng f holds
X = Y

proof end;

theorem :: FUNCT_1:162

for X being set
for A being Subset of X holds (id X) .: A = A

proof end;

definition

let f be Function;
redefine attr f is empty-yielding means :: FUNCT_1:def 14
for x being set st x in dom f holds
f . x is empty;
compatibility

proof end;

end;

:: deftheorem defines empty-yielding FUNCT_1:def 14 :

registration

cluster empty-yielding set ;
existence by RELAT_1:60;

end;

definition

let F be Function;
redefine attr F is non-empty means :Def15: :: FUNCT_1:def 15
for n being set st n in dom F holds
not F . n is empty;
compatibility

proof end;

end;

:: deftheorem Def15 defines non-empty FUNCT_1:def 15 :

registration

cluster non-empty set ;
existence

proof end;

end;

scheme :: FUNCT_1:sch 4
LambdaB{ F₁() -> non empty set , F₂( set ) -> set } :

ex f being Function st
( dom f = F₁() & ( for d being Element of F₁() holds f . d = F₂(d) ) )

proof end;

registration

let f be non-empty Function;
cluster rng f -> with_non-empty_elements ;
coherence

proof end;

end;