:: RFUNCT_2 semantic presentation

theorem :: RFUNCT_2:1

canceled;

theorem :: RFUNCT_2:2

for F, G being Function
for X being set holds (G | (F .: X)) * (F | X) = (G * F) | X

proof end;

theorem :: RFUNCT_2:3

for F, G being Function
for X, X1 being set holds (G | X1) * (F | X) = (G * F) | (X /\ (F " X1))

proof end;

theorem Th4: :: RFUNCT_2:4

for F, G being Function
for X being set holds
( X c= dom (G * F) iff ( X c= dom F & F .: X c= dom G ) )

proof end;

theorem :: RFUNCT_2:5

for F being Function
for X being set holds (F | X) .: X = F .: X

proof end;

definition

let seq be Real_Sequence;
:: original: rng
redefine func rng seq -> Subset of REAL ;
coherence by RELSET_1:12;

end;

theorem Th6: :: RFUNCT_2:6

for seq1, seq2, seq3 being Real_Sequence holds
( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) )

proof end;

theorem Th7: :: RFUNCT_2:7

for seq being Real_Sequence
for n being Element of NAT holds rng (seq ^\ n) c= rng seq

proof end;

theorem Th8: :: RFUNCT_2:8

for seq being Real_Sequence
for n being Element of NAT
for h being PartFunc of REAL , REAL st rng seq c= dom h holds
seq . n in dom h

proof end;

theorem Th9: :: RFUNCT_2:9

for x being set
for seq being Real_Sequence holds
( x in rng seq iff ex n being Element of NAT st x = seq . n )

proof end;

theorem :: RFUNCT_2:10

for seq being Real_Sequence
for n being Element of NAT holds seq . n in rng seq by Th9;

theorem Th11: :: RFUNCT_2:11

for seq1, seq being Real_Sequence st seq1 is subsequence of seq holds
rng seq1 c= rng seq

proof end;

theorem :: RFUNCT_2:12

for seq1, seq being Real_Sequence st seq1 is subsequence of seq & seq is_not_0 holds
seq1 is_not_0

proof end;

theorem Th13: :: RFUNCT_2:13

for seq1, seq2 being Real_Sequence
for Ns being increasing Seq_of_Nat holds
( (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) & (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) )

proof end;

theorem Th14: :: RFUNCT_2:14

for p being Element of REAL
for seq being Real_Sequence
for Ns being increasing Seq_of_Nat holds (p (#) seq) * Ns = p (#) (seq * Ns)

proof end;

theorem :: RFUNCT_2:15

for seq being Real_Sequence
for Ns being increasing Seq_of_Nat holds
( (- seq) * Ns = - (seq * Ns) & (abs seq) * Ns = abs (seq * Ns) )

proof end;

theorem Th16: :: RFUNCT_2:16

for seq being Real_Sequence
for Ns being increasing Seq_of_Nat holds (seq * Ns) " = (seq " ) * Ns

proof end;

theorem :: RFUNCT_2:17

for seq1, seq being Real_Sequence
for Ns being increasing Seq_of_Nat holds (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns)

proof end;

theorem :: RFUNCT_2:18

for seq being Real_Sequence st seq is convergent & ( for n being Element of NAT holds seq . n <= 0 ) holds
lim seq <= 0

proof end;

theorem :: RFUNCT_2:19

for Y being set
for seq being Real_Sequence st ( for n being Element of NAT holds seq . n in Y ) holds
rng seq c= Y

proof end;

definition

let h be PartFunc of REAL , REAL ;
let seq be Real_Sequence;
assume A1: rng seq c= dom h ;
func h * seq -> Real_Sequence equals :Def1: :: RFUNCT_2:def 1
h * seq;
coherence

proof end;

end;

:: deftheorem Def1 defines * RFUNCT_2:def 1 :

theorem :: RFUNCT_2:20

canceled;

theorem Th21: :: RFUNCT_2:21

for seq being Real_Sequence
for n being Element of NAT
for h being PartFunc of REAL , REAL st rng seq c= dom h holds
(h * seq) . n = h . (seq . n)

proof end;

theorem Th22: :: RFUNCT_2:22

for seq being Real_Sequence
for n being Element of NAT
for h being PartFunc of REAL , REAL st rng seq c= dom h holds
(h * seq) ^\ n = h * (seq ^\ n)

proof end;

theorem Th23: :: RFUNCT_2:23

for seq being Real_Sequence
for h1, h2 being PartFunc of REAL , REAL st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) * seq = (h1 * seq) + (h2 * seq) & (h1 - h2) * seq = (h1 * seq) - (h2 * seq) & (h1 (#) h2) * seq = (h1 * seq) (#) (h2 * seq) )

proof end;

theorem Th24: :: RFUNCT_2:24

for seq being Real_Sequence
for h being PartFunc of REAL , REAL
for r being real number st rng seq c= dom h holds
(r (#) h) * seq = r (#) (h * seq)

proof end;

theorem :: RFUNCT_2:25

for seq being Real_Sequence
for h being PartFunc of REAL , REAL st rng seq c= dom h holds
( abs (h * seq) = (abs h) * seq & - (h * seq) = (- h) * seq )

proof end;

theorem :: RFUNCT_2:26

for seq being Real_Sequence
for h being PartFunc of REAL , REAL st rng seq c= dom (h ^ ) holds
h * seq is_not_0

proof end;

theorem :: RFUNCT_2:27

for seq being Real_Sequence
for h being PartFunc of REAL , REAL st rng seq c= dom (h ^ ) holds
(h ^ ) * seq = (h * seq) "

proof end;

theorem Th28: :: RFUNCT_2:28

for seq being Real_Sequence
for Ns being increasing Seq_of_Nat
for h being PartFunc of REAL , REAL st rng seq c= dom h holds
(h * seq) * Ns = h * (seq * Ns)

proof end;

theorem :: RFUNCT_2:29

for seq1, seq2 being Real_Sequence
for h being PartFunc of REAL , REAL st rng seq1 c= dom h & seq2 is subsequence of seq1 holds
h * seq2 is subsequence of h * seq1

proof end;

theorem :: RFUNCT_2:30

for seq being Real_Sequence
for n being Element of NAT
for h being PartFunc of REAL , REAL st h is total holds
(h * seq) . n = h . (seq . n)

proof end;

theorem :: RFUNCT_2:31

for seq being Real_Sequence
for n being Element of NAT
for h being PartFunc of REAL , REAL st h is total holds
h * (seq ^\ n) = (h * seq) ^\ n

proof end;

theorem :: RFUNCT_2:32

for seq being Real_Sequence
for h1, h2 being PartFunc of REAL , REAL st h1 is total & h2 is total holds
( (h1 + h2) * seq = (h1 * seq) + (h2 * seq) & (h1 - h2) * seq = (h1 * seq) - (h2 * seq) & (h1 (#) h2) * seq = (h1 * seq) (#) (h2 * seq) )

proof end;

theorem :: RFUNCT_2:33

for r being Element of REAL
for seq being Real_Sequence
for h being PartFunc of REAL , REAL st h is total holds
(r (#) h) * seq = r (#) (h * seq)

proof end;

theorem :: RFUNCT_2:34

for X being set
for seq being Real_Sequence
for h being PartFunc of REAL , REAL st rng seq c= dom (h | X) holds
(h | X) * seq = h * seq

proof end;

theorem :: RFUNCT_2:35

for X, Y being set
for seq being Real_Sequence
for h being PartFunc of REAL , REAL st rng seq c= dom (h | X) & ( rng seq c= dom (h | Y) or X c= Y ) holds
(h | X) * seq = (h | Y) * seq

proof end;

theorem :: RFUNCT_2:36

for X being set
for seq being Real_Sequence
for h being PartFunc of REAL , REAL st rng seq c= dom (h | X) holds
abs ((h | X) * seq) = ((abs h) | X) * seq

proof end;

theorem :: RFUNCT_2:37

for X being set
for seq being Real_Sequence
for h being PartFunc of REAL , REAL st rng seq c= dom (h | X) & h " {0} = {} holds
((h ^ ) | X) * seq = ((h | X) * seq) "

proof end;

theorem Th38: :: RFUNCT_2:38

for seq being Real_Sequence
for h being PartFunc of REAL , REAL st rng seq c= dom h holds
h .: (rng seq) = rng (h * seq)

proof end;

theorem :: RFUNCT_2:39

for seq being Real_Sequence
for h2, h1 being PartFunc of REAL , REAL st rng seq c= dom (h2 * h1) holds
h2 * (h1 * seq) = (h2 * h1) * seq

proof end;

registration

let Z be set ;
let f be one-to-one Function;
cluster f | Z -> one-to-one ;
coherence by FUNCT_1:84;

end;

theorem :: RFUNCT_2:40

for X being set
for h being one-to-one Function holds (h | X) " = (h " ) | (h .: X)

proof end;

theorem Th41: :: RFUNCT_2:41

for h being PartFunc of REAL , REAL st rng h is bounded & upper_bound (rng h) = lower_bound (rng h) holds
h is_constant_on dom h

proof end;

theorem :: RFUNCT_2:42

for Y being set
for h being PartFunc of REAL , REAL st Y c= dom h & h .: Y is bounded & upper_bound (h .: Y) = lower_bound (h .: Y) holds
h is_constant_on Y

proof end;

definition

let h be PartFunc of REAL , REAL ;
let Y be set ;
pred h is_increasing_on Y means :Def2: :: RFUNCT_2:def 2
for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 < h . r2;
pred h is_decreasing_on Y means :Def3: :: RFUNCT_2:def 3
for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 < h . r1;
pred h is_non_decreasing_on Y means :Def4: :: RFUNCT_2:def 4
for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2;
pred h is_non_increasing_on Y means :Def5: :: RFUNCT_2:def 5
for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 <= h . r1;

end;

:: deftheorem Def2 defines is_increasing_on RFUNCT_2:def 2 :

:: deftheorem Def3 defines is_decreasing_on RFUNCT_2:def 3 :

:: deftheorem Def4 defines is_non_decreasing_on RFUNCT_2:def 4 :

:: deftheorem Def5 defines is_non_increasing_on RFUNCT_2:def 5 :

definition

let h be PartFunc of REAL , REAL ;
let Y be set ;
pred h is_monotone_on Y means :Def6: :: RFUNCT_2:def 6
( h is_non_decreasing_on Y or h is_non_increasing_on Y );

end;

:: deftheorem Def6 defines is_monotone_on RFUNCT_2:def 6 :

theorem :: RFUNCT_2:43

canceled;

theorem :: RFUNCT_2:44

canceled;

theorem :: RFUNCT_2:45

canceled;

theorem :: RFUNCT_2:46

canceled;

theorem :: RFUNCT_2:47

canceled;

theorem Th48: :: RFUNCT_2:48

for Y being set
for h being PartFunc of REAL , REAL holds
( h is_non_decreasing_on Y iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r1 <= h . r2 )

proof end;

theorem Th49: :: RFUNCT_2:49

for Y being set
for h being PartFunc of REAL , REAL holds
( h is_non_increasing_on Y iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r2 <= h . r1 )

proof end;

theorem Th50: :: RFUNCT_2:50

for X being set
for h being PartFunc of REAL , REAL holds
( h is_increasing_on X iff h | X is_increasing_on X )

proof end;

theorem Th51: :: RFUNCT_2:51

for X being set
for h being PartFunc of REAL , REAL holds
( h is_decreasing_on X iff h | X is_decreasing_on X )

proof end;

theorem :: RFUNCT_2:52

for X being set
for h being PartFunc of REAL , REAL holds
( h is_non_decreasing_on X iff h | X is_non_decreasing_on X )

proof end;

theorem :: RFUNCT_2:53

for X being set
for h being PartFunc of REAL , REAL holds
( h is_non_increasing_on X iff h | X is_non_increasing_on X )

proof end;

theorem :: RFUNCT_2:54

for Y being set
for h being PartFunc of REAL , REAL st Y misses dom h holds
( h is_increasing_on Y & h is_decreasing_on Y & h is_non_decreasing_on Y & h is_non_increasing_on Y & h is_monotone_on Y )

proof end;

theorem :: RFUNCT_2:55

for Y being set
for h being PartFunc of REAL , REAL st h is_increasing_on Y holds
h is_non_decreasing_on Y

proof end;

theorem :: RFUNCT_2:56

for Y being set
for h being PartFunc of REAL , REAL st h is_decreasing_on Y holds
h is_non_increasing_on Y

proof end;

theorem :: RFUNCT_2:57

for Y being set
for h being PartFunc of REAL , REAL st h is_constant_on Y holds
h is_non_decreasing_on Y

proof end;

theorem :: RFUNCT_2:58

for Y being set
for h being PartFunc of REAL , REAL st h is_constant_on Y holds
h is_non_increasing_on Y

proof end;

theorem :: RFUNCT_2:59

for Y, X being set
for h being PartFunc of REAL , REAL st h is_non_decreasing_on Y & h is_non_increasing_on X holds
h is_constant_on Y /\ X

proof end;

theorem :: RFUNCT_2:60

for X, Y being set
for h being PartFunc of REAL , REAL st X c= Y & h is_increasing_on Y holds
h is_increasing_on X

proof end;

theorem :: RFUNCT_2:61

for X, Y being set
for h being PartFunc of REAL , REAL st X c= Y & h is_decreasing_on Y holds
h is_decreasing_on X

proof end;

theorem :: RFUNCT_2:62

for X, Y being set
for h being PartFunc of REAL , REAL st X c= Y & h is_non_decreasing_on Y holds
h is_non_decreasing_on X

proof end;

theorem :: RFUNCT_2:63

for X, Y being set
for h being PartFunc of REAL , REAL st X c= Y & h is_non_increasing_on Y holds
h is_non_increasing_on X

proof end;

theorem Th64: :: RFUNCT_2:64

for Y being set
for r being Element of REAL
for h being PartFunc of REAL , REAL holds
( ( h is_increasing_on Y & 0 < r implies r (#) h is_increasing_on Y ) & ( r = 0 implies r (#) h is_constant_on Y ) & ( h is_increasing_on Y & r < 0 implies r (#) h is_decreasing_on Y ) )

proof end;

theorem :: RFUNCT_2:65

for Y being set
for r being Element of REAL
for h being PartFunc of REAL , REAL holds
( ( h is_decreasing_on Y & 0 < r implies r (#) h is_decreasing_on Y ) & ( h is_decreasing_on Y & r < 0 implies r (#) h is_increasing_on Y ) )

proof end;

theorem Th66: :: RFUNCT_2:66

for Y being set
for r being Element of REAL
for h being PartFunc of REAL , REAL holds
( ( h is_non_decreasing_on Y & 0 <= r implies r (#) h is_non_decreasing_on Y ) & ( h is_non_decreasing_on Y & r <= 0 implies r (#) h is_non_increasing_on Y ) )

proof end;

theorem :: RFUNCT_2:67

for Y being set
for r being Element of REAL
for h being PartFunc of REAL , REAL holds
( ( h is_non_increasing_on Y & 0 <= r implies r (#) h is_non_increasing_on Y ) & ( h is_non_increasing_on Y & r <= 0 implies r (#) h is_non_decreasing_on Y ) )

proof end;

theorem Th68: :: RFUNCT_2:68

for X, Y being set
for r being Element of REAL
for h1, h2 being PartFunc of REAL , REAL st r in (X /\ Y) /\ (dom (h1 + h2)) holds
( r in X /\ (dom h1) & r in Y /\ (dom h2) )

proof end;

theorem :: RFUNCT_2:69

for X, Y being set
for h1, h2 being PartFunc of REAL , REAL holds
( ( h1 is_increasing_on X & h2 is_increasing_on Y implies h1 + h2 is_increasing_on X /\ Y ) & ( h1 is_decreasing_on X & h2 is_decreasing_on Y implies h1 + h2 is_decreasing_on X /\ Y ) & ( h1 is_non_decreasing_on X & h2 is_non_decreasing_on Y implies h1 + h2 is_non_decreasing_on X /\ Y ) & ( h1 is_non_increasing_on X & h2 is_non_increasing_on Y implies h1 + h2 is_non_increasing_on X /\ Y ) )

proof end;

theorem :: RFUNCT_2:70

for X, Y being set
for h1, h2 being PartFunc of REAL , REAL holds
( ( h1 is_increasing_on X & h2 is_constant_on Y implies h1 + h2 is_increasing_on X /\ Y ) & ( h1 is_decreasing_on X & h2 is_constant_on Y implies h1 + h2 is_decreasing_on X /\ Y ) )

proof end;

theorem :: RFUNCT_2:71

for X, Y being set
for h1, h2 being PartFunc of REAL , REAL st h1 is_increasing_on X & h2 is_non_decreasing_on Y holds
h1 + h2 is_increasing_on X /\ Y

proof end;

theorem :: RFUNCT_2:72

for X, Y being set
for h1, h2 being PartFunc of REAL , REAL st h1 is_non_increasing_on X & h2 is_constant_on Y holds
h1 + h2 is_non_increasing_on X /\ Y

proof end;

theorem :: RFUNCT_2:73

for X, Y being set
for h1, h2 being PartFunc of REAL , REAL st h1 is_decreasing_on X & h2 is_non_increasing_on Y holds
h1 + h2 is_decreasing_on X /\ Y

proof end;

theorem :: RFUNCT_2:74

for X, Y being set
for h1, h2 being PartFunc of REAL , REAL st h1 is_non_decreasing_on X & h2 is_constant_on Y holds
h1 + h2 is_non_decreasing_on X /\ Y

proof end;

theorem :: RFUNCT_2:75

for x being set
for h being PartFunc of REAL , REAL holds h is_increasing_on {x}

proof end;

theorem :: RFUNCT_2:76

for x being set
for h being PartFunc of REAL , REAL holds h is_decreasing_on {x}

proof end;

theorem :: RFUNCT_2:77

for x being set
for h being PartFunc of REAL , REAL holds h is_non_decreasing_on {x}

proof end;

theorem :: RFUNCT_2:78

for x being set
for h being PartFunc of REAL , REAL holds h is_non_increasing_on {x}

proof end;

theorem :: RFUNCT_2:79

for R being Subset of REAL holds id R is_increasing_on R

proof end;

theorem :: RFUNCT_2:80

for X being set
for h being PartFunc of REAL , REAL st h is_increasing_on X holds
- h is_decreasing_on X

proof end;

theorem :: RFUNCT_2:81

for X being set
for h being PartFunc of REAL , REAL st h is_non_decreasing_on X holds
- h is_non_increasing_on X

proof end;

theorem :: RFUNCT_2:82

for p, g being Element of REAL
for h being PartFunc of REAL , REAL st ( h is_increasing_on [.p,g.] or h is_decreasing_on [.p,g.] ) holds
h | [.p,g.] is one-to-one

proof end;

theorem :: RFUNCT_2:83

for p, g being Element of REAL
for h being one-to-one PartFunc of REAL , REAL st h is_increasing_on [.p,g.] holds
(h | [.p,g.]) " is_increasing_on h .: [.p,g.]

proof end;

theorem :: RFUNCT_2:84

for p, g being Element of REAL
for h being one-to-one PartFunc of REAL , REAL st h is_decreasing_on [.p,g.] holds
(h | [.p,g.]) " is_decreasing_on h .: [.p,g.]

proof end;