let X, Y be 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 ) )
let h1, h2 be PartFunc of REAL,REAL; ( ( 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 ) )
thus
( 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
assume that A1:
h1 | X is
increasing
and A2:
h2 | Y is
increasing
;
(h1 + h2) | (X /\ Y) is increasing
now for r1, r2 being Real st r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 holds
(h1 + h2) . r1 < (h1 + h2) . r2let r1,
r2 be
Real;
( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r1 < (h1 + h2) . r2 )assume that A3:
r1 in (X /\ Y) /\ (dom (h1 + h2))
and A4:
r2 in (X /\ Y) /\ (dom (h1 + h2))
and A5:
r1 < r2
;
(h1 + h2) . r1 < (h1 + h2) . r2
(
r1 in Y /\ (dom h2) &
r2 in Y /\ (dom h2) )
by A3, A4, Th36;
then A6:
h2 . r1 < h2 . r2
by A2, A5, Th20;
A7:
r1 in dom (h1 + h2)
by A3, XBOOLE_0:def 4;
(
r1 in X /\ (dom h1) &
r2 in X /\ (dom h1) )
by A3, A4, Th36;
then
h1 . r1 < h1 . r2
by A1, A5, Th20;
then
(h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2)
by A6, XREAL_1:8;
then A8:
(h1 + h2) . r1 < (h1 . r2) + (h2 . r2)
by A7, VALUED_1:def 1;
r2 in dom (h1 + h2)
by A4, XBOOLE_0:def 4;
hence
(h1 + h2) . r1 < (h1 + h2) . r2
by A8, VALUED_1:def 1;
verum end;
hence
(h1 + h2) | (X /\ Y) is
increasing
by Th20;
verum
end;
thus
( 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
assume that A9:
h1 | X is
decreasing
and A10:
h2 | Y is
decreasing
;
(h1 + h2) | (X /\ Y) is decreasing
now for r1, r2 being Real st r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 holds
(h1 + h2) . r2 < (h1 + h2) . r1let r1,
r2 be
Real;
( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r2 < (h1 + h2) . r1 )assume that A11:
r1 in (X /\ Y) /\ (dom (h1 + h2))
and A12:
r2 in (X /\ Y) /\ (dom (h1 + h2))
and A13:
r1 < r2
;
(h1 + h2) . r2 < (h1 + h2) . r1
(
r1 in Y /\ (dom h2) &
r2 in Y /\ (dom h2) )
by A11, A12, Th36;
then A14:
h2 . r2 < h2 . r1
by A10, A13, Th21;
A15:
r2 in dom (h1 + h2)
by A12, XBOOLE_0:def 4;
(
r1 in X /\ (dom h1) &
r2 in X /\ (dom h1) )
by A11, A12, Th36;
then
h1 . r2 < h1 . r1
by A9, A13, Th21;
then
(h1 . r2) + (h2 . r2) < (h1 . r1) + (h2 . r1)
by A14, XREAL_1:8;
then A16:
(h1 + h2) . r2 < (h1 . r1) + (h2 . r1)
by A15, VALUED_1:def 1;
r1 in dom (h1 + h2)
by A11, XBOOLE_0:def 4;
hence
(h1 + h2) . r2 < (h1 + h2) . r1
by A16, VALUED_1:def 1;
verum end;
hence
(h1 + h2) | (X /\ Y) is
decreasing
by Th21;
verum
end;
thus
( 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
assume that A17:
h1 | X is
non-decreasing
and A18:
h2 | Y is
non-decreasing
;
(h1 + h2) | (X /\ Y) is non-decreasing
now for r1, r2 being Real st r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 holds
(h1 + h2) . r1 <= (h1 + h2) . r2let r1,
r2 be
Real;
( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r1 <= (h1 + h2) . r2 )assume that A19:
r1 in (X /\ Y) /\ (dom (h1 + h2))
and A20:
r2 in (X /\ Y) /\ (dom (h1 + h2))
and A21:
r1 < r2
;
(h1 + h2) . r1 <= (h1 + h2) . r2
(
r1 in Y /\ (dom h2) &
r2 in Y /\ (dom h2) )
by A19, A20, Th36;
then A22:
h2 . r1 <= h2 . r2
by A18, A21, Th22;
A23:
r1 in dom (h1 + h2)
by A19, XBOOLE_0:def 4;
(
r1 in X /\ (dom h1) &
r2 in X /\ (dom h1) )
by A19, A20, Th36;
then
h1 . r1 <= h1 . r2
by A17, A21, Th22;
then
(h1 . r1) + (h2 . r1) <= (h1 . r2) + (h2 . r2)
by A22, XREAL_1:7;
then A24:
(h1 + h2) . r1 <= (h1 . r2) + (h2 . r2)
by A23, VALUED_1:def 1;
r2 in dom (h1 + h2)
by A20, XBOOLE_0:def 4;
hence
(h1 + h2) . r1 <= (h1 + h2) . r2
by A24, VALUED_1:def 1;
verum end;
hence
(h1 + h2) | (X /\ Y) is
non-decreasing
by Th22;
verum
end;
assume that
A25:
h1 | X is non-increasing
and
A26:
h2 | Y is non-increasing
; (h1 + h2) | (X /\ Y) is non-increasing
now for r1, r2 being Real st r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 holds
(h1 + h2) . r2 <= (h1 + h2) . r1let r1,
r2 be
Real;
( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r2 <= (h1 + h2) . r1 )assume that A27:
r1 in (X /\ Y) /\ (dom (h1 + h2))
and A28:
r2 in (X /\ Y) /\ (dom (h1 + h2))
and A29:
r1 < r2
;
(h1 + h2) . r2 <= (h1 + h2) . r1
(
r1 in Y /\ (dom h2) &
r2 in Y /\ (dom h2) )
by A27, A28, Th36;
then A30:
h2 . r2 <= h2 . r1
by A26, A29, Th23;
A31:
r2 in dom (h1 + h2)
by A28, XBOOLE_0:def 4;
(
r1 in X /\ (dom h1) &
r2 in X /\ (dom h1) )
by A27, A28, Th36;
then
h1 . r2 <= h1 . r1
by A25, A29, Th23;
then
(h1 . r2) + (h2 . r2) <= (h1 . r1) + (h2 . r1)
by A30, XREAL_1:7;
then A32:
(h1 + h2) . r2 <= (h1 . r1) + (h2 . r1)
by A31, VALUED_1:def 1;
r1 in dom (h1 + h2)
by A27, XBOOLE_0:def 4;
hence
(h1 + h2) . r2 <= (h1 + h2) . r1
by A32, VALUED_1:def 1;
verum end;
hence
(h1 + h2) | (X /\ Y) is non-increasing
by Th23; verum