:: Properties of Real Functions
:: by Jaros{\l}aw Kotowicz
::
:: Received June 18, 1990
:: Copyright (c) 1990 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 b1 being PartFunc of REAL,REAL st b1 is non-decreasing holds
b1 is monotone
by Def6;
cluster Function-like non-increasing -> monotone Element of K21(K22(REAL,REAL));
coherence
for b1 being PartFunc of REAL,REAL st b1 is non-increasing holds
b1 is monotone
by Def6;
cluster Function-like non monotone -> non non-decreasing non non-increasing Element of K21(K22(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 :: 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 b1 being PartFunc of REAL,REAL st b1 is non-decreasing & b1 is non-increasing holds
b1 is constant
proof end;
end;

registration
cluster Function-like V8() -> non-decreasing non-increasing Element of K21(K22(REAL,REAL));
coherence
for b1 being PartFunc of REAL,REAL st b1 is constant holds
( b1 is non-increasing & b1 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 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 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 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 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: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;