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


::
:: REAL SEQUENCES
::
theorem Th1: :: RFUNCT_2:1
for seq1, seq2, seq3 being Real_Sequence holds
( seq1 = seq2 - seq3 iff for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) )
proof end;

theorem Th2: :: RFUNCT_2:2
for seq1, seq2 being Real_Sequence
for Ns being V43() 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 Th3: :: RFUNCT_2:3
for p being Real
for seq being Real_Sequence
for Ns being V43() sequence of NAT holds (p (#) seq) * Ns = p (#) (seq * Ns)
proof end;

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

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

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

theorem :: RFUNCT_2:7
for seq being Real_Sequence st seq is convergent & ( for n being Nat holds seq . n <= 0 ) holds
lim seq <= 0
proof end;

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) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
proof end;

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 st rng seq c= dom h holds
(r (#) h) /* seq = r (#) (h /* seq)
proof end;

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 & - (h /* seq) = (- h) /* seq )
proof end;

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
proof end;

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) "
proof end;

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 & 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:14
for r being 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)
proof end;

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
proof end;

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) & h " {0} = {} holds
((h ^) | X) /* seq = ((h | X) /* seq) "
proof end;

::
:: MONOTONE FUNCTIONS
::
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:52;
end;

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

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

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 & upper_bound (h .: Y) = lower_bound (h .: Y) holds
h | Y is V8()
proof end;

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

:: deftheorem defines non-increasing RFUNCT_2:def 4 :
for h being PartFunc of REAL,REAL holds
( h is non-increasing iff for r1, r2 being Real st r1 in dom h & r2 in dom h & 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 Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 < h . r2 )
proof end;

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 Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 < h . r1 )
proof end;

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 Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2 )
proof end;

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 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 :: RFUNCT_2:def 5
( h is non-decreasing or h is non-increasing );
end;

:: deftheorem 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 ;
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 ;
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 & 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 Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r1 <= h . r2 )
proof end;

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 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() for Element of bool [:REAL,REAL:];
coherence
for b1 being PartFunc of REAL,REAL st b1 is non-decreasing & b1 is non-increasing holds
b1 is V8()
proof end;
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 & b1 is non-decreasing ) ;
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
proof end;
end;

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

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

registration
let h be non-decreasing PartFunc of REAL,REAL;
let X be set ;
cluster h | 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
proof end;
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 & h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone )
proof end;

theorem :: RFUNCT_2:27
for X, Y 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 V8()
proof end;

theorem :: RFUNCT_2:28
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:29
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:30
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:31
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 Th32: :: RFUNCT_2:32
for Y being set
for r being 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 V8() ) & ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing ) )
proof end;

theorem :: RFUNCT_2:33
for Y being set
for r being 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 Th34: :: RFUNCT_2:34
for Y being set
for r being 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:35
for Y being set
for r being 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 Th36: :: RFUNCT_2:36
for X, Y being set
for r being 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:37
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:38
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL holds
( ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing ) )
proof end;

theorem :: RFUNCT_2:39
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:40
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-increasing & h2 | Y is V8() holds
(h1 + h2) | (X /\ Y) is non-increasing
proof end;

theorem :: RFUNCT_2:41
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:42
for X, Y being set
for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-decreasing & h2 | Y is V8() holds
(h1 + h2) | (X /\ Y) is non-decreasing
proof end;

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

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

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

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

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

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 by Th32;

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 by Th34;

theorem :: RFUNCT_2:50
for g, p being 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:51
for g, p being 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:52
for g, p being 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;