:: Properties of Real Functions
:: by Jaros{\l}aw Kotowicz
::
:: Received June 18, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

theorem :: RFUNCT_2:1

canceled;

theorem :: RFUNCT_2:2

canceled;

theorem :: RFUNCT_2:3

canceled;

theorem :: RFUNCT_2:4

canceled;

theorem :: RFUNCT_2:5

canceled;

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

canceled;

theorem :: RFUNCT_2:8

canceled;

theorem :: RFUNCT_2:9

canceled;

theorem :: RFUNCT_2:10

canceled;

theorem :: RFUNCT_2:11

canceled;

theorem :: RFUNCT_2:12

canceled;

theorem Th13: :: RFUNCT_2:13

for seq1, seq2 being Real_Sequence
for Ns being V33() sequence 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 V33() sequence of NAT holds (p (#) seq) * Ns = p (#) (seq * Ns)

proof end;

theorem :: RFUNCT_2:15

for seq being Real_Sequence
for Ns being V33() sequence 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 V33() sequence of NAT holds (seq * Ns) " = (seq ") * Ns

proof end;

theorem :: RFUNCT_2:17

for seq1, seq being Real_Sequence
for Ns being V33() sequence 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

canceled;

theorem :: RFUNCT_2:20

canceled;

theorem :: RFUNCT_2:21

canceled;

theorem :: RFUNCT_2:22

canceled;

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

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

canceled;

theorem :: RFUNCT_2:29

canceled;

theorem :: RFUNCT_2:30

canceled;

theorem :: RFUNCT_2:31

canceled;

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

canceled;

theorem :: RFUNCT_2:35

canceled;

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;

registration

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

end;

theorem :: RFUNCT_2:38

canceled;

theorem :: RFUNCT_2:39

canceled;

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

proof end;

theorem :: RFUNCT_2:42

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

proof end;

definition

canceled;
let h be PartFunc of REAL,REAL;
redefine attr h is increasing means :Def2: :: RFUNCT_2:def 2
for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 < h . r2;
compatibility
( h is increasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 < h . r2 )

proof end;

redefine attr h is decreasing means :Def3: :: RFUNCT_2:def 3
for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 < h . r1;
compatibility
( h is decreasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 < h . r1 )

proof end;

redefine attr h is non-decreasing means :Def4: :: RFUNCT_2:def 4
for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 <= h . r2;
compatibility
( h is non-decreasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 <= h . r2 )

proof end;

redefine attr h is non-increasing means :Def5: :: RFUNCT_2:def 5
for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 <= h . r1;
compatibility
( h is non-increasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 <= h . r1 )

proof end;

end;

:: deftheorem RFUNCT_2:def 1 :
canceled;

:: deftheorem Def2 defines increasing RFUNCT_2:def 2 :
for h being PartFunc of REAL,REAL holds
( h is increasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 < h . r2 );

:: deftheorem Def3 defines decreasing RFUNCT_2:def 3 :
for h being PartFunc of REAL,REAL holds
( h is decreasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 < h . r1 );

:: deftheorem Def4 defines non-decreasing RFUNCT_2:def 4 :
for h being PartFunc of REAL,REAL holds
( h is non-decreasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 <= h . r2 );

:: deftheorem Def5 defines non-increasing RFUNCT_2:def 5 :
for h being PartFunc of REAL,REAL holds
( h is non-increasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 <= h . r1 );

theorem Th43: :: RFUNCT_2:43

for Y being set
for h being PartFunc of REAL,REAL holds
( h | Y is increasing 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 Th44: :: RFUNCT_2:44

for Y being set
for h being PartFunc of REAL,REAL holds
( h | Y is decreasing 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 Th45: :: RFUNCT_2:45

for Y being set
for h being PartFunc of REAL,REAL holds
( h | Y is non-decreasing 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 Th46: :: RFUNCT_2:46

for Y being set
for h being PartFunc of REAL,REAL holds
( h | Y is non-increasing 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;

definition

let h be PartFunc of REAL,REAL;
attr h is monotone means :Def6: :: RFUNCT_2:def 6
( h is non-decreasing or h is non-increasing );

end;

:: deftheorem Def6 defines monotone RFUNCT_2:def 6 :
for h being PartFunc of REAL,REAL holds
( h is monotone iff ( h is non-decreasing or h is non-increasing ) );

registration

cluster Function-like non-decreasing -> monotone Element of K21(K22(REAL,REAL));
coherence
for b₁ being PartFunc of REAL,REAL st b₁ is non-decreasing holds
b₁ is monotone by Def6;
cluster Function-like non-increasing -> monotone Element of K21(K22(REAL,REAL));
coherence
for b₁ being PartFunc of REAL,REAL st b₁ is non-increasing holds
b₁ is monotone by Def6;
cluster Function-like non monotone -> non non-decreasing non non-increasing Element of K21(K22(REAL,REAL));
coherence
for b₁ being PartFunc of REAL,REAL st not b₁ is monotone holds
( not b₁ is non-decreasing & not b₁ is non-increasing ) ;

end;

theorem :: RFUNCT_2:47

canceled;

theorem Th48: :: RFUNCT_2:48

for Y being set
for h being PartFunc of REAL,REAL holds
( h | Y is non-decreasing 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 | Y is non-increasing 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;

registration

cluster Function-like non-decreasing non-increasing -> V8() Element of K21(K22(REAL,REAL));
coherence
for b₁ being PartFunc of REAL,REAL st b₁ is non-decreasing & b₁ is non-increasing holds
b₁ is constant

proof end;

end;

registration

cluster Function-like V8() -> non-decreasing non-increasing Element of K21(K22(REAL,REAL));
coherence
for b₁ being PartFunc of REAL,REAL st b₁ is constant holds
( b₁ is non-increasing & b₁ is non-decreasing )

proof end;

end;

registration

cluster Relation-like REAL -defined REAL -valued Function-like trivial complex-valued ext-real-valued real-valued Element of K21(K22(REAL,REAL));
existence
ex b₁ being PartFunc of REAL,REAL st b₁ is trivial

proof end;

end;

registration

let h be increasing PartFunc of REAL,REAL;
let X be set ;
cluster h | X -> increasing PartFunc of REAL,REAL;
coherence
for b₁ being PartFunc of REAL,REAL st b₁ = h | X holds
b₁ is increasing

proof end;

end;

registration

let h be decreasing PartFunc of REAL,REAL;
let X be set ;
cluster h | X -> decreasing PartFunc of REAL,REAL;
coherence
for b₁ being PartFunc of REAL,REAL st b₁ = h | X holds
b₁ is decreasing

proof end;

end;

registration

let h be non-decreasing PartFunc of REAL,REAL;
let X be set ;
cluster h | X -> non-decreasing PartFunc of REAL,REAL;
coherence
for b₁ being PartFunc of REAL,REAL st b₁ = h | X holds
b₁ is non-decreasing

proof end;

end;

theorem :: RFUNCT_2:50

canceled;

theorem :: RFUNCT_2:51

canceled;

theorem :: RFUNCT_2:52

canceled;

theorem :: RFUNCT_2:53

canceled;

theorem :: RFUNCT_2:54

for Y being set
for h being PartFunc of REAL,REAL st Y misses dom h holds
( h | Y is increasing & h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone )

proof end;

theorem :: RFUNCT_2:55

canceled;

theorem :: RFUNCT_2:56

canceled;

theorem :: RFUNCT_2:57

canceled;

theorem :: RFUNCT_2:58

canceled;

theorem :: RFUNCT_2:59

for Y, X being set
for h being PartFunc of REAL,REAL st h | Y is non-decreasing & h | X is non-increasing holds
h | (Y /\ X) is constant

proof end;

theorem :: RFUNCT_2:60

for X, Y being set
for h being PartFunc of REAL,REAL st X c= Y & h | Y is increasing holds
h | X is increasing

proof end;

theorem :: RFUNCT_2:61

for X, Y being set
for h being PartFunc of REAL,REAL st X c= Y & h | Y is decreasing holds
h | X is decreasing

proof end;

theorem :: RFUNCT_2:62

for X, Y being set
for h being PartFunc of REAL,REAL st X c= Y & h | Y is non-decreasing holds
h | X is non-decreasing

proof end;

theorem :: RFUNCT_2:63

for X, Y being set
for h being PartFunc of REAL,REAL st X c= Y & h | Y is non-increasing holds
h | X is non-increasing

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 | Y is increasing & 0 < r implies (r (#) h) | Y is increasing ) & ( r = 0 implies (r (#) h) | Y is constant ) & ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing ) )

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 | Y is decreasing & 0 < r implies (r (#) h) | Y is decreasing ) & ( h | Y is decreasing & r < 0 implies (r (#) h) | Y is increasing ) )

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 | Y is non-decreasing & 0 <= r implies (r (#) h) | Y is non-decreasing ) & ( h | Y is non-decreasing & r <= 0 implies (r (#) h) | Y is non-increasing ) )

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 | Y is non-increasing & 0 <= r implies (r (#) h) | Y is non-increasing ) & ( h | Y is non-increasing & r <= 0 implies (r (#) h) | Y is non-decreasing ) )

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 | X is increasing & h2 | Y is increasing implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is decreasing implies (h1 + h2) | (X /\ Y) is decreasing ) & ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) & ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing ) )

proof end;

theorem :: RFUNCT_2:70

for X, Y being set
for h1, h2 being PartFunc of REAL,REAL holds
( ( h1 | X is increasing & h2 | Y is constant implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is constant implies (h1 + h2) | (X /\ Y) is decreasing ) )

proof end;

theorem :: RFUNCT_2:71

for X, Y being set
for h1, h2 being PartFunc of REAL,REAL st h1 | X is increasing & h2 | Y is non-decreasing holds
(h1 + h2) | (X /\ Y) is increasing

proof end;

theorem :: RFUNCT_2:72

for X, Y being set
for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-increasing & h2 | Y is constant holds
(h1 + h2) | (X /\ Y) is non-increasing

proof end;

theorem :: RFUNCT_2:73

for X, Y being set
for h1, h2 being PartFunc of REAL,REAL st h1 | X is decreasing & h2 | Y is non-increasing holds
(h1 + h2) | (X /\ Y) is decreasing

proof end;

theorem :: RFUNCT_2:74

for X, Y being set
for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-decreasing & h2 | Y is constant holds
(h1 + h2) | (X /\ Y) is non-decreasing

proof end;

theorem :: RFUNCT_2:75

for x being set
for h being PartFunc of REAL,REAL holds h | {x} is non-increasing

proof end;

theorem :: RFUNCT_2:76

for x being set
for h being PartFunc of REAL,REAL holds h | {x} is decreasing

proof end;

theorem :: RFUNCT_2:77

for x being set
for h being PartFunc of REAL,REAL holds h | {x} is non-decreasing

proof end;

theorem :: RFUNCT_2:78

for x being set
for h being PartFunc of REAL,REAL holds h | {x} is non-increasing

proof end;

theorem :: RFUNCT_2:79

for R being Subset of REAL holds (id R) | R is increasing

proof end;

theorem :: RFUNCT_2:80

for X being set
for h being PartFunc of REAL,REAL st h | X is increasing holds
(- h) | X is decreasing

proof end;

theorem :: RFUNCT_2:81

for X being set
for h being PartFunc of REAL,REAL st h | X is non-decreasing holds
(- h) | X is non-increasing

proof end;

theorem :: RFUNCT_2:82

for p, g being Element of REAL
for h being PartFunc of REAL,REAL st ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) 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 | [.p,g.] is increasing holds
((h | [.p,g.]) ") | (h .: [.p,g.]) is increasing

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 | [.p,g.] is decreasing holds
((h | [.p,g.]) ") | (h .: [.p,g.]) is decreasing

proof end;