let Y be 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 ) )
let r be 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 ) )
let h be PartFunc of REAL,REAL; ( ( 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 ) )
thus
( 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
assume that A1:
h | Y is
non-decreasing
and A2:
0 <= r
;
(r (#) h) | Y is non-decreasing
now for r1, r2 being Real st r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 holds
(r (#) h) . r1 <= (r (#) h) . r2let r1,
r2 be
Real;
( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r1 <= (r (#) h) . r2 )assume that A3:
r1 in Y /\ (dom (r (#) h))
and A4:
r2 in Y /\ (dom (r (#) h))
and A5:
r1 < r2
;
(r (#) h) . r1 <= (r (#) h) . r2A6:
r2 in Y
by A4, XBOOLE_0:def 4;
A7:
r2 in dom (r (#) h)
by A4, XBOOLE_0:def 4;
then
r2 in dom h
by VALUED_1:def 5;
then A8:
r2 in Y /\ (dom h)
by A6, XBOOLE_0:def 4;
A9:
r1 in Y
by A3, XBOOLE_0:def 4;
A10:
r1 in dom (r (#) h)
by A3, XBOOLE_0:def 4;
then
r1 in dom h
by VALUED_1:def 5;
then
r1 in Y /\ (dom h)
by A9, XBOOLE_0:def 4;
then
h . r1 <= h . r2
by A1, A5, A8, Th22;
then
r * (h . r1) <= (h . r2) * r
by A2, XREAL_1:64;
then
(r (#) h) . r1 <= r * (h . r2)
by A10, VALUED_1:def 5;
hence
(r (#) h) . r1 <= (r (#) h) . r2
by A7, VALUED_1:def 5;
verum end;
hence
(r (#) h) | Y is
non-decreasing
by Th22;
verum
end;
assume that
A11:
h | Y is non-decreasing
and
A12:
r <= 0
; (r (#) h) | Y is non-increasing
now for r1, r2 being Real st r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 holds
(r (#) h) . r2 <= (r (#) h) . r1let r1,
r2 be
Real;
( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r2 <= (r (#) h) . r1 )assume that A13:
r1 in Y /\ (dom (r (#) h))
and A14:
r2 in Y /\ (dom (r (#) h))
and A15:
r1 < r2
;
(r (#) h) . r2 <= (r (#) h) . r1A16:
r2 in Y
by A14, XBOOLE_0:def 4;
A17:
r2 in dom (r (#) h)
by A14, XBOOLE_0:def 4;
then
r2 in dom h
by VALUED_1:def 5;
then A18:
r2 in Y /\ (dom h)
by A16, XBOOLE_0:def 4;
A19:
r1 in Y
by A13, XBOOLE_0:def 4;
A20:
r1 in dom (r (#) h)
by A13, XBOOLE_0:def 4;
then
r1 in dom h
by VALUED_1:def 5;
then
r1 in Y /\ (dom h)
by A19, XBOOLE_0:def 4;
then
h . r1 <= h . r2
by A11, A15, A18, Th22;
then
r * (h . r2) <= r * (h . r1)
by A12, XREAL_1:65;
then
(r (#) h) . r2 <= r * (h . r1)
by A17, VALUED_1:def 5;
hence
(r (#) h) . r2 <= (r (#) h) . r1
by A20, VALUED_1:def 5;
verum end;
hence
(r (#) h) | Y is non-increasing
by Th23; verum