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


begin

::
:: REAL SEQUENCES
::
theorem Th1: :: RFUNCT_2:1
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) )
proofend;

theorem Th2: :: RFUNCT_2:2
for seq1, seq2 being Real_Sequence
for Ns being V37() 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) )
proofend;

theorem Th3: :: RFUNCT_2:3
for p being Element of REAL
for seq being Real_Sequence
for Ns being V37() sequence of NAT holds (p (#) seq) * Ns = p (#) (seq * Ns)
proofend;

theorem :: RFUNCT_2:4
for seq being Real_Sequence
for Ns being V37() sequence of NAT holds
( (- seq) * Ns = - (seq * Ns) & (abs seq) * Ns = abs (seq * Ns) )
proofend;

theorem Th5: :: RFUNCT_2:5
for seq being Real_Sequence
for Ns being V37() sequence of NAT holds (seq * Ns) " = (seq ") * Ns
proofend;

theorem :: RFUNCT_2:6
for seq1, seq being Real_Sequence
for Ns being V37() sequence of NAT holds (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns)
proofend;

theorem :: RFUNCT_2:7
for seq being Real_Sequence st seq is convergent &amp; ( for n being Element of NAT holds seq . n <= 0 ) holds
lim seq <= 0
proofend;

theorem Th8: :: RFUNCT_2:8
for W being non empty set
for h1, h2 being PartFunc of W,REAL
for seq being sequence of W st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) &amp; (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) &amp; (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
proofend;

theorem Th9: :: RFUNCT_2:9
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W
for r being real number st rng seq c= dom h holds
(r (#) h) /* seq = r (#) (h /* seq)
proofend;

theorem :: RFUNCT_2:10
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom h holds
( abs (h /* seq) = (abs h) /* seq &amp; - (h /* seq) = (- h) /* seq )
proofend;

theorem :: RFUNCT_2:11
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h ^) holds
h /* seq is non-zero
proofend;

theorem :: RFUNCT_2:12
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h ^) holds
(h ^) /* seq = (h /* seq) "
proofend;

theorem :: RFUNCT_2:13
for W being non empty set
for h1, h2 being PartFunc of W,REAL
for seq being sequence of W st h1 is total &amp; h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) &amp; (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) &amp; (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
proofend;

theorem :: RFUNCT_2:14
for r being Element of REAL
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st h is total holds
(r (#) h) /* seq = r (#) (h /* seq)
proofend;

theorem :: RFUNCT_2:15
for X being set
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h | X) holds
abs ((h | X) /* seq) = ((abs h) | X) /* seq
proofend;

theorem :: RFUNCT_2:16
for X being set
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h | X) &amp; h " {0} = {} holds
((h ^) | X) /* seq = ((h | X) /* seq) "
proofend;

::
:: MONOTONE FUNCTIONS
::
registration
let Z be set ;
let f be one-to-one Function;
clusterf | Z ->  one-to-one ;
coherence
 f | Z is one-to-one by FUNCT_1:52;
end;

theorem :: RFUNCT_2:17
for X being set
for h being one-to-one Function holds (h | X) " = (h ") | (h .: X)
proofend;

theorem Th18: :: RFUNCT_2:18
for W being non empty set
for h being PartFunc of W,REAL st rng h is real-bounded &amp; upper_bound (rng h) = lower_bound (rng h) holds
h is V8()
proofend;

theorem :: RFUNCT_2:19
for Y being set
for W being non empty set
for h being PartFunc of W,REAL st h .: Y is real-bounded &amp; upper_bound (h .: Y) = lower_bound (h .: Y) holds
h | Y is V8()
proofend;

definition
let h be PartFunc of REAL,REAL;
redefine attr h is increasing  means :Def1: :: RFUNCT_2:def 1
 for r1, r2 being Element of REAL st r1 in dom h &amp; r2 in dom h &amp; r1 < r2 holds
h . r1 < h . r2;
compatibility
 ( h is increasing iff for r1, r2 being Element of REAL st r1 in dom h &amp; r2 in dom h &amp; r1 < r2 holds
h . r1 < h . r2 )
proofend;
redefine attr h is decreasing  means :Def2: :: RFUNCT_2:def 2
 for r1, r2 being Element of REAL st r1 in dom h &amp; r2 in dom h &amp; r1 < r2 holds
h . r2 < h . r1;
compatibility
 ( h is decreasing iff for r1, r2 being Element of REAL st r1 in dom h &amp; r2 in dom h &amp; r1 < r2 holds
h . r2 < h . r1 )
proofend;
redefine attr h is non-decreasing  means :Def3: :: RFUNCT_2:def 3
 for r1, r2 being Element of REAL st r1 in dom h &amp; r2 in dom h &amp; 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 &amp; r2 in dom h &amp; r1 < r2 holds
h . r1 <= h . r2 )
proofend;
redefine attr h is non-increasing  means :Def4: :: RFUNCT_2:def 4
 for r1, r2 being Element of REAL st r1 in dom h &amp; r2 in dom h &amp; 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 &amp; r2 in dom h &amp; r1 < r2 holds
h . r2 <= h . r1 )
proofend;
end;

:: deftheorem Def1 defines increasing RFUNCT_2:def_1_:_
 for h being PartFunc of REAL,REAL holds
( h is increasing iff for r1, r2 being Element of REAL st r1 in dom h &amp; r2 in dom h &amp; r1 < r2 holds
h . r1 < h . r2 );

:: deftheorem Def2 defines decreasing RFUNCT_2:def_2_:_
 for h being PartFunc of REAL,REAL holds
( h is decreasing iff for r1, r2 being Element of REAL st r1 in dom h &amp; r2 in dom h &amp; r1 < r2 holds
h . r2 < h . r1 );

:: deftheorem Def3 defines non-decreasing RFUNCT_2:def_3_:_
 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 &amp; r2 in dom h &amp; r1 < r2 holds
h . r1 <= h . r2 );

:: deftheorem Def4 defines non-increasing RFUNCT_2:def_4_:_
 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 &amp; r2 in dom h &amp; r1 < r2 holds
h . r2 <= h . r1 );

theorem Th20: :: RFUNCT_2:20
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) &amp; r2 in Y /\ (dom h) &amp; r1 < r2 holds
h . r1 < h . r2 )
proofend;

theorem Th21: :: RFUNCT_2:21
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) &amp; r2 in Y /\ (dom h) &amp; r1 < r2 holds
h . r2 < h . r1 )
proofend;

theorem Th22: :: RFUNCT_2:22
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) &amp; r2 in Y /\ (dom h) &amp; r1 < r2 holds
h . r1 <= h . r2 )
proofend;

theorem Th23: :: RFUNCT_2:23
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) &amp; r2 in Y /\ (dom h) &amp; r1 < r2 holds
h . r2 <= h . r1 )
proofend;

definition
let h be PartFunc of REAL,REAL;
attrh is monotone  means :Def5: :: RFUNCT_2:def 5
( h is non-decreasing or h is non-increasing );
end;

:: deftheorem Def5 defines monotone RFUNCT_2:def_5_:_
 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 for Element of bool [:REAL,REAL:];
coherence
 for b1 being PartFunc of REAL,REAL st b1 is non-decreasing holds
b1 is monotone by Def5;
cluster Function-like non-increasing  ->  monotone for Element of bool [:REAL,REAL:];
coherence
 for b1 being PartFunc of REAL,REAL st b1 is non-increasing holds
b1 is monotone by Def5;
cluster Function-like non monotone  ->  non non-decreasing non non-increasing for Element of bool [:REAL,REAL:];
coherence
 for b1 being PartFunc of REAL,REAL st not b1 is monotone holds
( not b1 is non-decreasing &amp; not b1 is non-increasing ) ;
end;

theorem Th24: :: RFUNCT_2:24
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) &amp; r2 in Y /\ (dom h) &amp; r1 <= r2 holds
h . r1 <= h . r2 )
proofend;

theorem Th25: :: RFUNCT_2:25
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) &amp; r2 in Y /\ (dom h) &amp; r1 <= r2 holds
h . r2 <= h . r1 )
proofend;

registration
cluster Function-like non-decreasing non-increasing  -> V8() for Element of bool [:REAL,REAL:];
coherence
 for b1 being PartFunc of REAL,REAL st b1 is non-decreasing &amp; b1 is non-increasing holds
b1 is V8()
proofend;
end;

registration
cluster Function-like V8()  ->  non-decreasing non-increasing for Element of bool [:REAL,REAL:];
coherence
 for b1 being PartFunc of REAL,REAL st b1 is V8() holds
( b1 is non-increasing &amp; b1 is non-decreasing )
proofend;
end;

registration
cluster Relation-like REAL -defined REAL -valued Function-like trivial complex-valued ext-real-valued real-valued for Element of bool [:REAL,REAL:];
existence
 ex b1 being PartFunc of REAL,REAL st b1 is trivial
proofend;
end;

registration
let h be increasing PartFunc of REAL,REAL;
let X be set ;
clusterh | X ->  increasing for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = h | X holds
b1 is increasing
proofend;
end;

registration
let h be decreasing PartFunc of REAL,REAL;
let X be set ;
clusterh | X ->  decreasing for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = h | X holds
b1 is decreasing
proofend;
end;

registration
let h be non-decreasing PartFunc of REAL,REAL;
let X be set ;
clusterh | X ->  non-decreasing for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = h | X holds
b1 is non-decreasing
proofend;
end;

theorem :: RFUNCT_2:26
for Y being set
for h being PartFunc of REAL,REAL st Y misses dom h holds
( h | Y is increasing &amp; h | Y is decreasing &amp; h | Y is non-decreasing &amp; h | Y is non-increasing &amp; h | Y is monotone )
proofend;

theorem :: RFUNCT_2:27
for Y, X being set
for h being PartFunc of REAL,REAL st h | Y is non-decreasing &amp; h | X is non-increasing holds
h | (Y /\ X) is V8()
proofend;

theorem :: RFUNCT_2:28
for X, Y being set
for h being PartFunc of REAL,REAL st X c= Y &amp; h | Y is increasing holds
h | X is increasing
proofend;

theorem :: RFUNCT_2:29
for X, Y being set
for h being PartFunc of REAL,REAL st X c= Y &amp; h | Y is decreasing holds
h | X is decreasing
proofend;

theorem :: RFUNCT_2:30
for X, Y being set
for h being PartFunc of REAL,REAL st X c= Y &amp; h | Y is non-decreasing holds
h | X is non-decreasing
proofend;

theorem :: RFUNCT_2:31
for X, Y being set
for h being PartFunc of REAL,REAL st X c= Y &amp; h | Y is non-increasing holds
h | X is non-increasing
proofend;

theorem Th32: :: RFUNCT_2:32
for Y being set
for r being Element of REAL
for h being PartFunc of REAL,REAL holds
( ( h | Y is increasing &amp; 0 < r implies (r (#) h) | Y is increasing ) &amp; ( r = 0 implies (r (#) h) | Y is V8() ) &amp; ( h | Y is increasing &amp; r < 0 implies (r (#) h) | Y is decreasing ) )
proofend;

theorem :: RFUNCT_2:33
for Y being set
for r being Element of REAL
for h being PartFunc of REAL,REAL holds
( ( h | Y is decreasing &amp; 0 < r implies (r (#) h) | Y is decreasing ) &amp; ( h | Y is decreasing &amp; r < 0 implies (r (#) h) | Y is increasing ) )
proofend;

theorem Th34: :: RFUNCT_2:34
for Y being set
for r being Element of REAL
for h being PartFunc of REAL,REAL holds
( ( h | Y is non-decreasing &amp; 0 <= r implies (r (#) h) | Y is non-decreasing ) &amp; ( h | Y is non-decreasing &amp; r <= 0 implies (r (#) h) | Y is non-increasing ) )
proofend;

theorem :: RFUNCT_2:35
for Y being set
for r being Element of REAL
for h being PartFunc of REAL,REAL holds
( ( h | Y is non-increasing &amp; 0 <= r implies (r (#) h) | Y is non-increasing ) &amp; ( h | Y is non-increasing &amp; r <= 0 implies (r (#) h) | Y is non-decreasing ) )
proofend;

theorem Th36: :: RFUNCT_2:36
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) &amp; r in Y /\ (dom h2) )
proofend;

theorem :: RFUNCT_2:37
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL holds
( ( h1 | X is increasing &amp; h2 | Y is increasing implies (h1 + h2) | (X /\ Y) is increasing ) &amp; ( h1 | X is decreasing &amp; h2 | Y is decreasing implies (h1 + h2) | (X /\ Y) is decreasing ) &amp; ( h1 | X is non-decreasing &amp; h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) &amp; ( h1 | X is non-increasing &amp; h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing ) )
proofend;

theorem :: RFUNCT_2:38
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL holds
( ( h1 | X is increasing &amp; h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) &amp; ( h1 | X is decreasing &amp; h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing ) )
proofend;

theorem :: RFUNCT_2:39
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL st h1 | X is increasing &amp; h2 | Y is non-decreasing holds
(h1 + h2) | (X /\ Y) is increasing
proofend;

theorem :: RFUNCT_2:40
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-increasing &amp; h2 | Y is V8() holds
(h1 + h2) | (X /\ Y) is non-increasing
proofend;

theorem :: RFUNCT_2:41
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL st h1 | X is decreasing &amp; h2 | Y is non-increasing holds
(h1 + h2) | (X /\ Y) is decreasing
proofend;

theorem :: RFUNCT_2:42
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-decreasing &amp; h2 | Y is V8() holds
(h1 + h2) | (X /\ Y) is non-decreasing
proofend;

theorem :: RFUNCT_2:43
for x being set
for h being PartFunc of REAL,REAL holds h | {x} is non-increasing
proofend;

theorem :: RFUNCT_2:44
for x being set
for h being PartFunc of REAL,REAL holds h | {x} is decreasing
proofend;

theorem :: RFUNCT_2:45
for x being set
for h being PartFunc of REAL,REAL holds h | {x} is non-decreasing
proofend;

theorem :: RFUNCT_2:46
for x being set
for h being PartFunc of REAL,REAL holds h | {x} is non-increasing
proofend;

theorem :: RFUNCT_2:47
for R being Subset of REAL holds (id R) | R is increasing
proofend;

theorem :: RFUNCT_2:48
for X being set
for h being PartFunc of REAL,REAL st h | X is increasing holds
(- h) | X is decreasing
proofend;

theorem :: RFUNCT_2:49
for X being set
for h being PartFunc of REAL,REAL st h | X is non-decreasing holds
(- h) | X is non-increasing
proofend;

theorem :: RFUNCT_2:50
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
proofend;

theorem :: RFUNCT_2:51
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
proofend;

theorem :: RFUNCT_2:52
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
proofend;