:: RFUNCT_1 semantic presentation

Lm1: (- 1) " = - 1
;

definition

let f1, f2 be real-yielding Function;
canceled;
canceled;
canceled;
func f1 / f2 -> Function means :Def4: :: RFUNCT_1:def 4
( dom it = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom it holds
it . c = (f1 . c) * ((f2 . c) " ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem RFUNCT_1:def 1 :

:: deftheorem RFUNCT_1:def 2 :

:: deftheorem RFUNCT_1:def 3 :

:: deftheorem Def4 defines / RFUNCT_1:def 4 :

registration

let f1, f2 be real-yielding Function;
cluster f1 / f2 -> real-yielding ;
coherence

proof end;

end;

definition

let C be set ;
let D be real-membered set ;
let f1, f2 be PartFunc of C,D;
:: original: /
redefine func f1 / f2 -> PartFunc of C, REAL ;
coherence

proof end;

end;

definition

let f be real-yielding Function;
canceled;
canceled;
canceled;
func f ^ -> Function means :Def8: :: RFUNCT_1:def 8
( dom it = (dom f) \ (f " {0}) & ( for c being set st c in dom it holds
it . c = (f . c) " ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem RFUNCT_1:def 5 :

:: deftheorem RFUNCT_1:def 6 :

:: deftheorem RFUNCT_1:def 7 :

:: deftheorem Def8 defines ^ RFUNCT_1:def 8 :

registration

let f be real-yielding Function;
cluster f ^ -> real-yielding ;
coherence

proof end;

end;

definition

let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original: ^
redefine func f ^ -> PartFunc of C, REAL ;
coherence

proof end;

end;

theorem :: RFUNCT_1:1

canceled;

theorem :: RFUNCT_1:2

canceled;

theorem :: RFUNCT_1:3

canceled;

theorem :: RFUNCT_1:4

canceled;

theorem :: RFUNCT_1:5

canceled;

theorem :: RFUNCT_1:6

canceled;

theorem :: RFUNCT_1:7

canceled;

theorem :: RFUNCT_1:8

canceled;

theorem :: RFUNCT_1:9

canceled;

theorem :: RFUNCT_1:10

canceled;

theorem Th11: :: RFUNCT_1:11

for g being real-yielding Function holds
( dom (g ^ ) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) )

proof end;

theorem Th12: :: RFUNCT_1:12

for f1, f2 being real-yielding Function holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0}))

proof end;

theorem Th13: :: RFUNCT_1:13

for C being non empty set
for c being Element of C
for f being real-yielding Function st c in dom (f ^ ) holds
f . c <> 0

proof end;

theorem Th14: :: RFUNCT_1:14

for f being real-yielding Function holds (f ^ ) " {0} = {}

proof end;

theorem Th15: :: RFUNCT_1:15

for f being real-yielding Function holds
( (abs f) " {0} = f " {0} & (- f) " {0} = f " {0} )

proof end;

theorem Th16: :: RFUNCT_1:16

for f being real-yielding Function holds dom ((f ^ ) ^ ) = dom (f | (dom (f ^ )))

proof end;

theorem Th17: :: RFUNCT_1:17

for f being real-yielding Function
for r being real number st r <> 0 holds
(r (#) f) " {0} = f " {0}

proof end;

theorem :: RFUNCT_1:18

canceled;

theorem :: RFUNCT_1:19

for f1, f2, f3 being real-yielding Function holds (f1 + f2) + f3 = f1 + (f2 + f3)

proof end;

theorem :: RFUNCT_1:20

canceled;

theorem Th21: :: RFUNCT_1:21

for f1, f2, f3 being real-yielding Function holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)

proof end;

theorem Th22: :: RFUNCT_1:22

for f1, f2, f3 being real-yielding Function holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)

proof end;

theorem :: RFUNCT_1:23

for f3, f1, f2 being real-yielding Function holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) by Th22;

theorem Th24: :: RFUNCT_1:24

for f1, f2 being real-yielding Function
for r being real number holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2

proof end;

theorem Th25: :: RFUNCT_1:25

for f1, f2 being real-yielding Function
for r being real number holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)

proof end;

theorem Th26: :: RFUNCT_1:26

for f1, f2, f3 being real-yielding Function holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)

proof end;

theorem :: RFUNCT_1:27

for f3, f1, f2 being real-yielding Function holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) by Th26;

theorem :: RFUNCT_1:28

for f1, f2 being real-yielding Function
for r being real number holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)

proof end;

theorem Th29: :: RFUNCT_1:29

for f being real-yielding Function
for r, p being real number holds (r * p) (#) f = r (#) (p (#) f)

proof end;

theorem :: RFUNCT_1:30

for f1, f2 being real-yielding Function
for r being real number holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)

proof end;

theorem :: RFUNCT_1:31

for f1, f2 being real-yielding Function holds f1 - f2 = (- 1) (#) (f2 - f1)

proof end;

theorem :: RFUNCT_1:32

for f1, f2, f3 being real-yielding Function holds f1 - (f2 + f3) = (f1 - f2) - f3

proof end;

theorem Th33: :: RFUNCT_1:33

for f being real-yielding Function holds 1 (#) f = f

proof end;

theorem :: RFUNCT_1:34

for f1, f2, f3 being real-yielding Function holds f1 - (f2 - f3) = (f1 - f2) + f3

proof end;

theorem :: RFUNCT_1:35

for f1, f2, f3 being real-yielding Function holds f1 + (f2 - f3) = (f1 + f2) - f3

proof end;

theorem Th36: :: RFUNCT_1:36

for f1, f2 being real-yielding Function holds abs (f1 (#) f2) = (abs f1) (#) (abs f2)

proof end;

theorem :: RFUNCT_1:37

for f being real-yielding Function
for r being real number holds abs (r (#) f) = (abs r) (#) (abs f)

proof end;

theorem Th38: :: RFUNCT_1:38

for f being real-yielding Function holds - f = (- 1) (#) f

proof end;

theorem Th39: :: RFUNCT_1:39

for f being real-yielding Function holds - (- f) = f

proof end;

theorem Th40: :: RFUNCT_1:40

for f1, f2 being real-yielding Function holds f1 - f2 = f1 + (- f2)

proof end;

theorem :: RFUNCT_1:41

for f1, f2 being real-yielding Function holds f1 - (- f2) = f1 + f2

proof end;

theorem Th42: :: RFUNCT_1:42

for f being real-yielding Function holds (f ^ ) ^ = f | (dom (f ^ ))

proof end;

theorem Th43: :: RFUNCT_1:43

for f1, f2 being real-yielding Function holds (f1 (#) f2) ^ = (f1 ^ ) (#) (f2 ^ )

proof end;

theorem Th44: :: RFUNCT_1:44

for f being real-yielding Function
for r being real number st r <> 0 holds
(r (#) f) ^ = (r " ) (#) (f ^ )

proof end;

theorem Th45: :: RFUNCT_1:45

for f being real-yielding Function holds (- f) ^ = (- 1) (#) (f ^ )

proof end;

theorem Th46: :: RFUNCT_1:46

for f being real-yielding Function holds (abs f) ^ = abs (f ^ )

proof end;

theorem Th47: :: RFUNCT_1:47

for f, g being real-yielding Function holds f / g = f (#) (g ^ )

proof end;

theorem Th48: :: RFUNCT_1:48

for g, f being real-yielding Function
for r being real number holds r (#) (g / f) = (r (#) g) / f

proof end;

theorem :: RFUNCT_1:49

for f, g being real-yielding Function holds (f / g) (#) g = f | (dom (g ^ ))

proof end;

theorem Th50: :: RFUNCT_1:50

for f, g, f1, g1 being real-yielding Function holds (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1)

proof end;

theorem Th51: :: RFUNCT_1:51

for f1, f2 being real-yielding Function holds (f1 / f2) ^ = (f2 | (dom (f2 ^ ))) / f1

proof end;

theorem Th52: :: RFUNCT_1:52

for g, f1, f2 being real-yielding Function holds g (#) (f1 / f2) = (g (#) f1) / f2

proof end;

theorem :: RFUNCT_1:53

for g, f1, f2 being real-yielding Function holds g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^ )))) / f1

proof end;

theorem :: RFUNCT_1:54

for f, g being real-yielding Function holds
( - (f / g) = (- f) / g & f / (- g) = - (f / g) )

proof end;

theorem :: RFUNCT_1:55

for f1, f, f2 being real-yielding Function holds
( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f )

proof end;

theorem Th56: :: RFUNCT_1:56

for f1, f, g1, g being real-yielding Function holds (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)

proof end;

theorem :: RFUNCT_1:57

for f, g, f1, g1 being real-yielding Function holds (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^ )))) / (g (#) f1)

proof end;

theorem :: RFUNCT_1:58

for f1, f, g1, g being real-yielding Function holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)

proof end;

theorem :: RFUNCT_1:59

for f1, f2 being real-yielding Function holds abs (f1 / f2) = (abs f1) / (abs f2)

proof end;

theorem Th60: :: RFUNCT_1:60

for X being set
for f1, f2 being real-yielding Function holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )

proof end;

theorem Th61: :: RFUNCT_1:61

for X being set
for f1, f2 being real-yielding Function holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )

proof end;

theorem Th62: :: RFUNCT_1:62

for X being set
for f being real-yielding Function holds
( (- f) | X = - (f | X) & (f ^ ) | X = (f | X) ^ & (abs f) | X = abs (f | X) )

proof end;

theorem :: RFUNCT_1:63

for X being set
for f1, f2 being real-yielding Function holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )

proof end;

theorem :: RFUNCT_1:64

for X being set
for f1, f2 being real-yielding Function holds
( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) )

proof end;

theorem :: RFUNCT_1:65

for X being set
for f being real-yielding Function
for r being real number holds (r (#) f) | X = r (#) (f | X)

proof end;

theorem Th66: :: RFUNCT_1:66

for C being non empty set
for f1, f2 being PartFunc of C, REAL holds
( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) )

proof end;

theorem Th67: :: RFUNCT_1:67

for C being non empty set
for r being real number
for f being PartFunc of C, REAL holds
( f is total iff r (#) f is total )

proof end;

theorem Th68: :: RFUNCT_1:68

for C being non empty set
for f being PartFunc of C, REAL holds
( f is total iff - f is total )

proof end;

theorem Th69: :: RFUNCT_1:69

for C being non empty set
for f being PartFunc of C, REAL holds
( f is total iff abs f is total )

proof end;

theorem Th70: :: RFUNCT_1:70

for C being non empty set
for f being PartFunc of C, REAL holds
( f ^ is total iff ( f " {0} = {} & f is total ) )

proof end;

theorem Th71: :: RFUNCT_1:71

for C being non empty set
for f1, f2 being PartFunc of C, REAL holds
( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total )

proof end;

theorem :: RFUNCT_1:72

for C being non empty set
for c being Element of C
for f1, f2 being PartFunc of C, REAL st f1 is total & f2 is total holds
( (f1 + f2) . c = (f1 . c) + (f2 . c) & (f1 - f2) . c = (f1 . c) - (f2 . c) & (f1 (#) f2) . c = (f1 . c) * (f2 . c) )

proof end;

theorem :: RFUNCT_1:73

for C being non empty set
for c being Element of C
for r being real number
for f being PartFunc of C, REAL st f is total holds
(r (#) f) . c = r * (f . c)

proof end;

theorem :: RFUNCT_1:74

for C being non empty set
for c being Element of C
for f being PartFunc of C, REAL st f is total holds
( (- f) . c = - (f . c) & (abs f) . c = abs (f . c) )

proof end;

theorem :: RFUNCT_1:75

for C being non empty set
for c being Element of C
for f being PartFunc of C, REAL st f ^ is total holds
(f ^ ) . c = (f . c) "

proof end;

theorem :: RFUNCT_1:76

for C being non empty set
for c being Element of C
for f1, f2 being PartFunc of C, REAL st f1 is total & f2 ^ is total holds
(f1 / f2) . c = (f1 . c) * ((f2 . c) " )

proof end;

definition

let X, C be set ;
:: original: chi
redefine func chi X,C -> PartFunc of C, REAL ;
coherence

proof end;

end;

theorem Th77: :: RFUNCT_1:77

for X being set
for C being non empty set
for f being PartFunc of C, REAL holds
( f = chi X,C iff ( dom f = C & ( for c being Element of C holds
( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) )

proof end;

theorem :: RFUNCT_1:78

for X being set
for C being non empty set holds chi X,C is total

proof end;

theorem :: RFUNCT_1:79

for X being set
for C being non empty set
for c being Element of C holds
( c in X iff (chi X,C) . c = 1 ) by Th77;

theorem :: RFUNCT_1:80

for X being set
for C being non empty set
for c being Element of C holds
( not c in X iff (chi X,C) . c = 0 ) by Th77;

theorem :: RFUNCT_1:81

for X being set
for C being non empty set
for c being Element of C holds
( c in C \ X iff (chi X,C) . c = 0 )

proof end;

theorem :: RFUNCT_1:82

canceled;

theorem :: RFUNCT_1:83

for C being non empty set
for c being Element of C holds (chi C,C) . c = 1 by Th77;

theorem Th84: :: RFUNCT_1:84

for X being set
for C being non empty set
for c being Element of C holds
( (chi X,C) . c <> 1 iff (chi X,C) . c = 0 )

proof end;

theorem :: RFUNCT_1:85

for X, Y being set
for C being non empty set st X misses Y holds
(chi X,C) + (chi Y,C) = chi (X \/ Y),C

proof end;

theorem :: RFUNCT_1:86

for X, Y being set
for C being non empty set holds (chi X,C) (#) (chi Y,C) = chi (X /\ Y),C

proof end;

definition

let f be real-yielding Function;
let Y be set ;
pred f is_bounded_above_on Y means :Def9: :: RFUNCT_1:def 9
ex r being real number st
for c being set st c in Y /\ (dom f) holds
f . c <= r;
pred f is_bounded_below_on Y means :Def10: :: RFUNCT_1:def 10
ex r being real number st
for c being set st c in Y /\ (dom f) holds
r <= f . c;

end;

:: deftheorem Def9 defines is_bounded_above_on RFUNCT_1:def 9 :

:: deftheorem Def10 defines is_bounded_below_on RFUNCT_1:def 10 :

definition

let f be real-yielding Function;
let Y be set ;
pred f is_bounded_on Y means :Def11: :: RFUNCT_1:def 11
( f is_bounded_above_on Y & f is_bounded_below_on Y );

end;

:: deftheorem Def11 defines is_bounded_on RFUNCT_1:def 11 :

theorem :: RFUNCT_1:87

canceled;

theorem :: RFUNCT_1:88

canceled;

theorem :: RFUNCT_1:89

canceled;

theorem Th90: :: RFUNCT_1:90

for Y being set
for f being real-yielding Function holds
( f is_bounded_on Y iff ex r being real number st
for c being set st c in Y /\ (dom f) holds
abs (f . c) <= r )

proof end;

theorem :: RFUNCT_1:91

for Y, X being set
for f being real-yielding Function holds
( ( Y c= X & f is_bounded_above_on X implies f is_bounded_above_on Y ) & ( Y c= X & f is_bounded_below_on X implies f is_bounded_below_on Y ) & ( Y c= X & f is_bounded_on X implies f is_bounded_on Y ) )

proof end;

theorem :: RFUNCT_1:92

for X, Y being set
for f being real-yielding Function st f is_bounded_above_on X & f is_bounded_below_on Y holds
f is_bounded_on X /\ Y

proof end;

theorem :: RFUNCT_1:93

for X being set
for f being real-yielding Function st X misses dom f holds
f is_bounded_on X

proof end;

theorem :: RFUNCT_1:94

for Y being set
for r being real number
for f being real-yielding Function st 0 = r holds
r (#) f is_bounded_on Y

proof end;

theorem Th95: :: RFUNCT_1:95

for Y being set
for r being real number
for f being real-yielding Function holds
( ( f is_bounded_above_on Y & 0 <= r implies r (#) f is_bounded_above_on Y ) & ( f is_bounded_above_on Y & r <= 0 implies r (#) f is_bounded_below_on Y ) )

proof end;

theorem Th96: :: RFUNCT_1:96

for Y being set
for r being real number
for f being real-yielding Function holds
( ( f is_bounded_below_on Y & 0 <= r implies r (#) f is_bounded_below_on Y ) & ( f is_bounded_below_on Y & r <= 0 implies r (#) f is_bounded_above_on Y ) )

proof end;

theorem Th97: :: RFUNCT_1:97

for Y being set
for r being real number
for f being real-yielding Function st f is_bounded_on Y holds
r (#) f is_bounded_on Y

proof end;

theorem :: RFUNCT_1:98

for X being set
for f being real-yielding Function holds abs f is_bounded_below_on X

proof end;

theorem Th99: :: RFUNCT_1:99

for Y being set
for f being real-yielding Function st f is_bounded_on Y holds
( abs f is_bounded_on Y & - f is_bounded_on Y )

proof end;

theorem Th100: :: RFUNCT_1:100

for X, Y being set
for f1, f2 being real-yielding Function holds
( ( f1 is_bounded_above_on X & f2 is_bounded_above_on Y implies f1 + f2 is_bounded_above_on X /\ Y ) & ( f1 is_bounded_below_on X & f2 is_bounded_below_on Y implies f1 + f2 is_bounded_below_on X /\ Y ) & ( f1 is_bounded_on X & f2 is_bounded_on Y implies f1 + f2 is_bounded_on X /\ Y ) )

proof end;

theorem Th101: :: RFUNCT_1:101

for X, Y being set
for f1, f2 being real-yielding Function st f1 is_bounded_on X & f2 is_bounded_on Y holds
( f1 (#) f2 is_bounded_on X /\ Y & f1 - f2 is_bounded_on X /\ Y )

proof end;

theorem Th102: :: RFUNCT_1:102

for X, Y being set
for f being real-yielding Function st f is_bounded_above_on X & f is_bounded_above_on Y holds
f is_bounded_above_on X \/ Y

proof end;

theorem Th103: :: RFUNCT_1:103

for X, Y being set
for f being real-yielding Function st f is_bounded_below_on X & f is_bounded_below_on Y holds
f is_bounded_below_on X \/ Y

proof end;

theorem :: RFUNCT_1:104

for X, Y being set
for f being real-yielding Function st f is_bounded_on X & f is_bounded_on Y holds
f is_bounded_on X \/ Y

proof end;

theorem :: RFUNCT_1:105

for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C, REAL st f1 is_constant_on X & f2 is_constant_on Y holds
( f1 + f2 is_constant_on X /\ Y & f1 - f2 is_constant_on X /\ Y & f1 (#) f2 is_constant_on X /\ Y )

proof end;

theorem Th106: :: RFUNCT_1:106

for Y being set
for C being non empty set
for p being real number
for f being PartFunc of C, REAL st f is_constant_on Y holds
p (#) f is_constant_on Y

proof end;

theorem Th107: :: RFUNCT_1:107

for Y being set
for C being non empty set
for f being PartFunc of C, REAL st f is_constant_on Y holds
( abs f is_constant_on Y & - f is_constant_on Y )

proof end;

theorem Th108: :: RFUNCT_1:108

for Y being set
for C being non empty set
for f being PartFunc of C, REAL st f is_constant_on Y holds
f is_bounded_on Y

proof end;

theorem :: RFUNCT_1:109

for Y being set
for C being non empty set
for f being PartFunc of C, REAL st f is_constant_on Y holds
( ( for r being real number holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & abs f is_bounded_on Y )

proof end;

theorem Th110: :: RFUNCT_1:110

for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C, REAL holds
( ( f1 is_bounded_above_on X & f2 is_constant_on Y implies f1 + f2 is_bounded_above_on X /\ Y ) & ( f1 is_bounded_below_on X & f2 is_constant_on Y implies f1 + f2 is_bounded_below_on X /\ Y ) & ( f1 is_bounded_on X & f2 is_constant_on Y implies f1 + f2 is_bounded_on X /\ Y ) )

proof end;

theorem :: RFUNCT_1:111

for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C, REAL holds
( ( f1 is_bounded_above_on X & f2 is_constant_on Y implies f1 - f2 is_bounded_above_on X /\ Y ) & ( f1 is_bounded_below_on X & f2 is_constant_on Y implies f1 - f2 is_bounded_below_on X /\ Y ) & ( f1 is_bounded_on X & f2 is_constant_on Y implies ( f1 - f2 is_bounded_on X /\ Y & f2 - f1 is_bounded_on X /\ Y & f1 (#) f2 is_bounded_on X /\ Y ) ) )

proof end;