let Y be set ; :: thesis: 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 )
let h be PartFunc of REAL,REAL; :: thesis: ( 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 )
thus ( h | Y is non-decreasing implies for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r1 <= h . r2 ) :: thesis: ( ( for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r1 <= h . r2 ) implies h | Y is non-decreasing )
proof
assume A1: h | Y is non-decreasing ; :: thesis: for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r1 <= h . r2
let r1, r2 be Real; :: thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 implies h . r1 <= h . r2 )
assume that
A2: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) and
A3: r1 <= r2 ; :: thesis: h . r1 <= h . r2
now :: thesis: h . r1 <= h . r2
per cases ( r1 < r2 or r1 = r2 ) by A3, XXREAL_0:1;
suppose r1 < r2 ; :: thesis: h . r1 <= h . r2
hence h . r1 <= h . r2 by A1, A2, Th22; :: thesis: verum
end;
suppose r1 = r2 ; :: thesis: h . r1 <= h . r2
hence h . r1 <= h . r2 ; :: thesis: verum
end;
end;
end;
hence h . r1 <= h . r2 ; :: thesis: verum
end;
assume A4: for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds
h . r1 <= h . r2 ; :: thesis: h | Y is non-decreasing
let r1 be Real; :: according to RFUNCT_2:def 3 :: thesis: for r2 being Real st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds
(h | Y) . r1 <= (h | Y) . r2
let r2 be Real; :: thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r1 <= (h | Y) . r2 )
assume that
A5: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and
A6: r1 < r2 ; :: thesis: (h | Y) . r1 <= (h | Y) . r2
A7: ( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by A5, FUNCT_1:47;
( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by A5, RELAT_1:61;
hence (h | Y) . r1 <= (h | Y) . r2 by A4, A6, A7; :: thesis: verum