:: by Jaros{\l}aw Kotowicz

::

:: Received June 18, 1990

:: Copyright (c) 1990-2019 Association of Mizar Users

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) )

( 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) )

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)

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) )

for Ns being V43() sequence of NAT holds

( (- seq) * Ns = - (seq * Ns) & (abs seq) * Ns = abs (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)

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

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) )

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)

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 )

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

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) "

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) )

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)

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

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) "

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

::

:: MONOTONE FUNCTIONS

::

registration
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()

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()

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;

( 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 ) ;

( 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 ) ;

( 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 )

( 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 )

end;
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 for r1, r2 being Real st r1 in dom h & r2 in dom h & r1 < r2 holds

h . r1 < h . r2;

( 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 for r1, r2 being Real st r1 in dom h & r2 in dom h & r1 < r2 holds

h . r2 < h . r1;

( 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 for r1, r2 being Real st r1 in dom h & r2 in dom h & r1 < r2 holds

h . r1 <= h . r2;

( 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 for r1, r2 being Real st r1 in dom h & r2 in dom h & r1 < r2 holds

h . r2 <= h . r1;

( 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;

:: 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 );

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 );

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 );

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 );

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 )

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 )

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 )

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 )

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;

:: 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 ) );

for h being PartFunc of REAL,REAL holds

( h is monotone iff ( h is non-decreasing or h is non-increasing ) );

registration

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} is non-decreasing holds

b_{1} is monotone
;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} is non-increasing holds

b_{1} is monotone
;

for b_{1} being PartFunc of REAL,REAL st not b_{1} is monotone holds

( not b_{1} is non-decreasing & not b_{1} is non-increasing )
;

end;
for b

b

coherence

for b

b

cluster Function-like non monotone -> non non-decreasing non non-increasing for Element of bool [:REAL,REAL:];

coherence for b

( not b

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 )

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 )

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

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} is non-decreasing & b_{1} is non-increasing holds

b_{1} is V8()

end;
for b

b

proof end;

registration

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} is V8() holds

( b_{1} is non-increasing & b_{1} is non-decreasing )
;

end;
for b

( b

registration

ex b_{1} being PartFunc of REAL,REAL st b_{1} is trivial
end;

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 b

proof end;

registration

let h be increasing PartFunc of REAL,REAL;

let X be set ;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = h | X holds

b_{1} is increasing

end;
let X be set ;

coherence

for b

b

proof end;

registration

let h be decreasing PartFunc of REAL,REAL;

let X be set ;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = h | X holds

b_{1} is decreasing

end;
let X be set ;

coherence

for b

b

proof end;

registration

let h be non-decreasing PartFunc of REAL,REAL;

let X be set ;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = h | X holds

b_{1} is non-decreasing

end;
let X be set ;

coherence

for b

b

proof 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 )

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()

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

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

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

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

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 ) )

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 ) )

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 ) )

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 ) )

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) )

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 ) )

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 ) )

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

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

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

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

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

for X being set

for h being PartFunc of REAL,REAL st h | X is increasing holds

(- h) | X is decreasing by Th32;

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;

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

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

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

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;

:: REAL SEQUENCES

::