:: Properties of Real Functions
:: by Jaros{\l}aw Kotowicz
::
:: Received June 18, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, SEQ_1, ORDINAL2, NAT_1, PARTFUN1, ARYTM_1,
FUNCT_1, ARYTM_3, RELAT_1, VALUED_1, COMPLEX1, SEQ_2, XXREAL_0, CARD_1,
REAL_1, TARSKI, XBOOLE_0, FUNCT_2, ORDINAL4, VALUED_0, XXREAL_2, SEQ_4,
SEQM_3, ZFMISC_1, XXREAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, RELSET_1,
PARTFUN1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, PARTFUN2,
RCOMP_1, RFUNCT_1, XXREAL_0, XXREAL_2, RECDEF_1;
constructors PARTFUN1, REAL_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3, SEQ_4, RCOMP_1,
PARTFUN2, RFUNCT_1, VALUED_1, RECDEF_1, XXREAL_2, ZFMISC_1, RELSET_1,
COMSEQ_2;
registrations FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED,
VALUED_0, VALUED_1, FUNCT_2, ZFMISC_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions XBOOLE_0, FUNCT_1, VALUED_0;
equalities XBOOLE_0, VALUED_1;
expansions XBOOLE_0, FUNCT_1, VALUED_0;
theorems TARSKI, FUNCT_1, SEQ_1, SEQ_2, SEQ_4, PARTFUN1, PARTFUN2, RFUNCT_1,
FUNCT_2, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0,
VALUED_1, VALUED_0, XREAL_0, ORDINAL1;
begin
reserve x,X,Y for set;
reserve g,r,r1,r2,p,p1,p2 for Real;
reserve R for Subset of REAL;
reserve seq,seq1,seq2,seq3 for Real_Sequence;
reserve Ns for increasing sequence of NAT;
reserve n for Nat;
reserve W for non empty set;
reserve h,h1,h2 for PartFunc of W,REAL;
::
:: REAL SEQUENCES
::
theorem Th1:
seq1=seq2-seq3 iff for n holds seq1.n=seq2.n-seq3.n
proof
thus seq1=seq2-seq3 implies for n holds seq1.n=seq2.n-seq3.n
proof
assume
A1: seq1=seq2-seq3;
now
let n;
seq1.n=seq2.n+(-seq3).n by A1,SEQ_1:7;
then seq1.n=seq2.n+-seq3.n by SEQ_1:10;
hence seq1.n=seq2.n-seq3.n;
end;
hence thesis;
end;
assume
A2: for n holds seq1.n=seq2.n-seq3.n;
now
let n;
thus seq1.n = seq2.n-seq3.n by A2
.= seq2.n+-seq3.n
.= seq2.n+(-seq3).n by SEQ_1:10;
end;
hence thesis by SEQ_1:7;
end;
theorem Th2:
(seq1 + seq2)*Ns = (seq1*Ns) + (seq2*Ns) & (seq1 - seq2)*Ns = (
seq1*Ns) - (seq2*Ns) & (seq1 (#) seq2)*Ns = (seq1*Ns) (#) (seq2*Ns)
proof
now
let n be Element of NAT;
thus ((seq1 + seq2)*Ns).n = (seq1 + seq2).(Ns.n) by FUNCT_2:15
.= seq1.(Ns.n) + seq2.(Ns.n) by SEQ_1:7
.= (seq1*Ns).n + seq2.(Ns.n) by FUNCT_2:15
.= (seq1*Ns).n + (seq2*Ns).n by FUNCT_2:15
.= (seq1*Ns + seq2*Ns).n by SEQ_1:7;
end;
hence (seq1 + seq2)*Ns = (seq1*Ns) + (seq2*Ns) by FUNCT_2:63;
now
let n be Element of NAT;
thus ((seq1 - seq2)*Ns).n = (seq1 - seq2).(Ns.n) by FUNCT_2:15
.= seq1.(Ns.n) - seq2.(Ns.n) by Th1
.= (seq1*Ns).n - seq2.(Ns.n) by FUNCT_2:15
.= (seq1*Ns).n - (seq2*Ns).n by FUNCT_2:15
.= (seq1*Ns - seq2*Ns).n by Th1;
end;
hence (seq1 - seq2)*Ns = (seq1*Ns) - (seq2*Ns) by FUNCT_2:63;
now
let n be Element of NAT;
thus ((seq1 (#) seq2)*Ns).n = (seq1 (#) seq2).(Ns.n) by FUNCT_2:15
.= seq1.(Ns.n) * seq2.(Ns.n) by SEQ_1:8
.= (seq1*Ns).n * seq2.(Ns.n) by FUNCT_2:15
.= (seq1*Ns).n * (seq2*Ns).n by FUNCT_2:15
.= ((seq1*Ns)(#)(seq2*Ns)).n by SEQ_1:8;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th3:
(p(#)seq)*Ns = p(#)(seq*Ns)
proof
now
let n be Element of NAT;
thus ((p(#)seq)*Ns).n = (p(#)seq).(Ns.n) by FUNCT_2:15
.= p*(seq.(Ns.n)) by SEQ_1:9
.= p*((seq*Ns).n) by FUNCT_2:15
.= (p(#)(seq*Ns)).n by SEQ_1:9;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(-seq)*Ns = -(seq*Ns) & (abs(seq))*Ns = abs((seq*Ns))
proof
thus (-seq)*Ns = ((-1)(#)seq)*Ns .= (-1)(#)(seq*Ns) by Th3
.= -(seq*Ns);
now
let n be Element of NAT;
thus ((abs(seq))*Ns).n = (abs(seq)).(Ns.n) by FUNCT_2:15
.= |.seq.(Ns.n).| by SEQ_1:12
.= |.(seq*Ns).n.| by FUNCT_2:15
.= (abs(seq*Ns)).n by SEQ_1:12;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th5:
(seq*Ns)" = (seq")*Ns
proof
now
let n be Element of NAT;
thus ((seq*Ns)").n = ((seq*Ns).n)" by VALUED_1:10
.= (seq.(Ns.n))" by FUNCT_2:15
.= (seq").(Ns.n) by VALUED_1:10
.= ((seq")*Ns).n by FUNCT_2:15;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(seq1/"seq)*Ns = (seq1*Ns)/"(seq*Ns)
proof
thus (seq1/"seq)*Ns = (seq1(#)(seq"))*Ns .= (seq1*Ns)(#)((seq")*Ns) by Th2
.= (seq1*Ns)(#)((seq*Ns)") by Th5
.= (seq1*Ns)/"(seq*Ns);
end;
theorem
seq is convergent & (for n holds seq.n<=0) implies lim seq <= 0
proof
assume that
A1: seq is convergent and
A2: for n holds seq.n<=0;
set seq1 = -seq;
A3: now
let n;
seq1.n = -seq.n & seq.n<=0 by A2,SEQ_1:10;
hence -(0 qua Real)<=seq1.n by XREAL_1:24;
end;
seq1 is convergent by A1,SEQ_2:9;
then 0 <= lim seq1 by A3,SEQ_2:17;
then -(0 qua Real) <= - lim seq by A1,SEQ_2:10;
hence thesis by XREAL_1:24;
end;
theorem Th8:
for h1,h2 being PartFunc of W,REAL, seq being sequence of W holds
rng seq c= dom h1 /\ dom h2 implies (h1+h2)/*seq=h1/*seq+h2/*seq
& (h1-h2)/*seq=h1/*seq-h2/*seq & (h1(#)h2)/*seq=(h1/*seq)(#)(h2/*seq)
proof
let h1,h2 be PartFunc of W,REAL, seq be sequence of W;
A1: dom h1 /\ dom h2 c= dom h1 by XBOOLE_1:17;
A2: dom h1 /\ dom h2 c= dom h2 by XBOOLE_1:17;
assume
A3: rng seq c= dom h1 /\ dom h2;
then
A4: rng seq c= dom (h1 + h2) by VALUED_1:def 1;
now
let n;
A5: n in NAT by ORDINAL1:def 12;
A6: seq.n in rng seq by VALUED_0:28;
thus ((h1+h2)/*seq).n = (h1+h2).(seq.n) by A4,FUNCT_2:108,A5
.= h1.(seq.n) + h2.(seq.n) by A4,A6,VALUED_1:def 1
.= (h1/*seq).n + h2.(seq.n) by A3,A1,FUNCT_2:108,XBOOLE_1:1,A5
.= (h1/*seq).n + (h2/*seq).n by A3,A2,FUNCT_2:108,XBOOLE_1:1,A5;
end;
hence (h1+h2)/*seq=h1/*seq+h2/*seq by SEQ_1:7;
A7: rng seq c= dom (h1 - h2) by A3,VALUED_1:12;
now
let n;
A8: n in NAT by ORDINAL1:def 12;
A9: seq.n in rng seq by VALUED_0:28;
thus ((h1-h2)/*seq).n = (h1-h2).(seq.n) by A7,FUNCT_2:108,A8
.= h1.(seq.n) - h2.(seq.n) by A7,A9,VALUED_1:13
.= (h1/*seq).n - h2.(seq.n) by A3,A1,FUNCT_2:108,XBOOLE_1:1,A8
.= (h1/*seq).n - (h2/*seq).n by A3,A2,FUNCT_2:108,XBOOLE_1:1,A8;
end;
hence (h1-h2)/*seq=h1/*seq-h2/*seq by Th1;
A10: rng seq c= dom (h1 (#) h2) by A3,VALUED_1:def 4;
now
let n;
A11: n in NAT by ORDINAL1:def 12;
thus ((h1(#)h2)/*seq).n = (h1(#)h2).(seq.n) by A10,FUNCT_2:108,A11
.= h1.(seq.n) * h2.(seq.n) by VALUED_1:5
.= (h1/*seq).n * h2.(seq.n) by A3,A1,FUNCT_2:108,XBOOLE_1:1,A11
.= (h1/*seq).n * (h2/*seq).n by A3,A2,FUNCT_2:108,XBOOLE_1:1,A11;
end;
hence thesis by SEQ_1:8;
end;
theorem Th9:
for h being PartFunc of W,REAL, seq being sequence of W holds
for r being Real holds rng seq c= dom h implies
(r(#)h)/*seq = r(#) (h/*seq)
proof
let h be PartFunc of W,REAL, seq be sequence of W;
let r be Real;
assume
A1: rng seq c= dom h;
then
A2: rng seq c= dom (r(#)h) by VALUED_1:def 5;
now
let n;
A3: n in NAT by ORDINAL1:def 12;
A4: seq.n in rng seq by VALUED_0:28;
thus ((r(#)h)/*seq).n = (r(#)h).(seq.n) by A2,FUNCT_2:108,A3
.= r * (h.(seq.n)) by A2,A4,VALUED_1:def 5
.= r * (h/*seq).n by A1,FUNCT_2:108,A3;
end;
hence thesis by SEQ_1:9;
end;
theorem
for h being PartFunc of W,REAL, seq being sequence of W holds
rng seq c= dom h implies abs(h/*seq) = (abs(h))/*seq & -(h/*seq) = (-h )/*seq
proof
let h be PartFunc of W,REAL, seq be sequence of W;
assume
A1: rng seq c= dom h;
then
A2: rng seq c= dom abs(h) by VALUED_1:def 11;
now
let n be Element of NAT;
thus abs(h/*seq).n = |.(h/*seq).n.| by SEQ_1:12
.= |.h.(seq.n).| by A1,FUNCT_2:108
.= abs(h).(seq.n) by VALUED_1:18
.= (abs(h)/*seq).n by A2,FUNCT_2:108;
end;
hence abs(h/*seq) = (abs(h))/*seq by FUNCT_2:63;
thus -(h/*seq) = (-1)(#)(h/*seq) .= ((-1)(#)h)/*seq by A1,Th9
.= (-h)/*seq;
end;
theorem
for h being PartFunc of W,REAL, seq being sequence of W holds
rng seq c= dom (h^) implies h/*seq is non-zero
proof
let h be PartFunc of W,REAL, seq be sequence of W;
assume
A1: rng seq c= dom (h^);
then
A2: dom h \ h"{0} c= dom h & rng seq c= dom h \ h"{0} by RFUNCT_1:def 2
,XBOOLE_1:36;
now
given n such that
A3: (h/*seq).n=0;
A4: n in NAT by ORDINAL1:def 12;
seq.n in rng seq by VALUED_0:28;
then seq.n in dom (h^) by A1;
then seq.n in dom h \ h"{0} by RFUNCT_1:def 2;
then seq.n in dom h & not seq.n in h"{0} by XBOOLE_0:def 5;
then
A5: not h.(seq.n) in {0} by FUNCT_1:def 7;
h.(seq.n) =0 by A2,A3,FUNCT_2:108,XBOOLE_1:1,A4;
hence contradiction by A5,TARSKI:def 1;
end;
hence thesis by SEQ_1:5;
end;
theorem
for h being PartFunc of W,REAL, seq being sequence of W holds
rng seq c= dom (h^) implies (h^)/*seq =(h/*seq)"
proof
let h be PartFunc of W,REAL, seq be sequence of W;
assume
A1: rng seq c= dom (h^);
then
A2: dom h \ h"{0} c= dom h & rng seq c= dom h \ h"{0} by RFUNCT_1:def 2
,XBOOLE_1:36;
now
let n be Element of NAT;
A3: seq.n in rng seq by VALUED_0:28;
thus ((h^)/*seq).n = (h^).(seq.n) by A1,FUNCT_2:108
.= (h.(seq.n))" by A1,A3,RFUNCT_1:def 2
.= ((h/*seq).n)" by A2,FUNCT_2:108,XBOOLE_1:1
.= ((h/*seq)").n by VALUED_1:10;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for h1,h2 being PartFunc of W,REAL, seq being sequence of W holds
h1 is total & h2 is total implies
(h1+h2)/*seq = h1/*seq + h2/*seq & (h1-h2)/*seq = h1/*seq - h2/*seq &
(h1(#)h2)/*seq = (h1/*seq) (#) (h2/*seq)
proof
let h1,h2 be PartFunc of W,REAL, seq be sequence of W;
assume h1 is total & h2 is total;
then dom (h1+h2) = W by PARTFUN1:def 2;
then dom h1 /\ dom h2 = W by VALUED_1:def 1;
then
A1: rng seq c= dom h1 /\ dom h2;
hence (h1+h2)/*seq = h1/*seq + h2/*seq by Th8;
thus (h1-h2)/*seq = h1/*seq - h2/*seq by A1,Th8;
thus thesis by A1,Th8;
end;
theorem
for h being PartFunc of W,REAL, seq being sequence of W holds
h is total implies (r(#)h)/*seq = r(#)(h/*seq)
proof
let h be PartFunc of W,REAL, seq be sequence of W;
assume h is total;
then dom h = W by PARTFUN1:def 2;
then rng seq c= dom h;
hence thesis by Th9;
end;
theorem
for h being PartFunc of W,REAL, seq being sequence of W holds
rng seq c= dom (h|X) implies abs((h|X)/*seq) = ((abs(h))|X)/*seq
proof
let h be PartFunc of W,REAL, seq be sequence of W;
assume
A1: rng seq c= dom (h|X);
A2: dom (h|X) = dom h /\ X by RELAT_1:61
.= dom abs(h) /\ X by VALUED_1:def 11
.= dom (abs(h)|X) by RELAT_1:61;
now
let n be Element of NAT;
A3: seq.n in rng seq by VALUED_0:28;
then seq.n in dom (h|X) by A1;
then seq.n in dom h /\ X by RELAT_1:61;
then
A4: seq.n in X by XBOOLE_0:def 4;
thus (abs((h|X)/*seq)).n = |. ((h|X)/*seq).n .| by SEQ_1:12
.= |. (h|X).(seq.n) .| by A1,FUNCT_2:108
.= |. h.(seq.n) .| by A1,A3,FUNCT_1:47
.= (abs(h)).(seq.n) by VALUED_1:18
.= ((abs(h))|X).(seq.n) by A4,FUNCT_1:49
.= (((abs(h))|X)/*seq).n by A1,A2,FUNCT_2:108;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for h being PartFunc of W,REAL, seq being sequence of W holds
rng seq c= dom (h|X) & h"{0}={} implies ((h^)|X)/*seq = ((h|X)/*seq)"
proof
let h be PartFunc of W,REAL, seq be sequence of W;
assume that
A1: rng seq c= dom (h|X) and
A2: h"{0}={};
now
let x be object;
assume x in rng seq;
then x in dom (h|X) by A1;
then
A3: x in dom h /\ X by RELAT_1:61;
then x in dom h \ h"{0} by A2,XBOOLE_0:def 4;
then
A4: x in dom (h^) by RFUNCT_1:def 2;
x in X by A3,XBOOLE_0:def 4;
then x in dom (h^) /\ X by A4,XBOOLE_0:def 4;
hence x in dom ((h^)|X) by RELAT_1:61;
end;
then
A5: rng seq c= dom ((h^)|X) by TARSKI:def 3;
now
let n be Element of NAT;
A6: seq.n in rng seq by VALUED_0:28;
then seq.n in dom (h|X) by A1;
then
A7: seq.n in dom h /\ X by RELAT_1:61;
then
A8: seq.n in X by XBOOLE_0:def 4;
seq.n in dom h \ h"{0} by A2,A7,XBOOLE_0:def 4;
then
A9: seq.n in dom (h^) by RFUNCT_1:def 2;
thus (((h^)|X)/*seq).n = ((h^)|X).(seq.n) by A5,FUNCT_2:108
.= (h^).(seq.n) by A8,FUNCT_1:49
.= (h.(seq.n))" by A9,RFUNCT_1:def 2
.= ((h|X).(seq.n))" by A1,A6,FUNCT_1:47
.= (((h|X)/*seq).n)" by A1,FUNCT_2:108
.= (((h|X)/*seq)").n by VALUED_1:10;
end;
hence thesis by FUNCT_2:63;
end;
::
:: MONOTONE FUNCTIONS
::
registration
let Z be set;
let f be one-to-one Function;
cluster f|Z -> one-to-one;
coherence by FUNCT_1:52;
end;
theorem
for h being one-to-one Function holds (h|X)" = (h")|(h.:X)
proof
let h be one-to-one Function;
reconsider hX = h|X as one-to-one Function;
now
let r be object;
thus r in dom ((h|X)") implies r in dom ((h")|(h.:X))
proof
assume r in dom ((h|X)");
then r in rng(hX) by FUNCT_1:33;
then consider g being object such that
A1: g in dom (h|X) and
A2: (h|X).g=r by FUNCT_1:def 3;
A3: h.g=r by A1,A2,FUNCT_1:47;
A4: g in dom h /\ X by A1,RELAT_1:61;
then g in dom h by XBOOLE_0:def 4;
then r in rng h by A3,FUNCT_1:def 3;
then
A5: r in dom (h") by FUNCT_1:33;
g in dom h & g in X by A4,XBOOLE_0:def 4;
then r in h.:X by A3,FUNCT_1:def 6;
then r in dom (h")/\(h.:X) by A5,XBOOLE_0:def 4;
hence thesis by RELAT_1:61;
end;
assume r in dom ((h")|(h.:X));
then r in dom(h") /\ (h.:X) by RELAT_1:61;
then r in h.:X by XBOOLE_0:def 4;
then consider t being object such that
A6: t in dom h and
A7: t in X and
A8: h.t=r by FUNCT_1:def 6;
t in dom h/\X by A6,A7,XBOOLE_0:def 4;
then
A9: t in dom(h|X) by RELAT_1:61;
(h|X).t=r by A7,A8,FUNCT_1:49;
then r in rng(hX) by A9,FUNCT_1:def 3;
hence r in dom((h|X)") by FUNCT_1:33;
end;
then
A10: dom ((hX)")=dom ((h")|(h.:X)) by TARSKI:2;
now
given r being object such that
A11: r in dom((h|X)") and
A12: ((h|X)").r<>((h")|(h.:X)).r;
r in dom(h")/\(h.:X) by A10,A11,RELAT_1:61;
then r in h.:X by XBOOLE_0:def 4;
then consider t be object such that
t in dom h and
t in X and
A13: h.t=r by FUNCT_1:def 6;
r in rng (hX) by A11,FUNCT_1:33;
then consider g be object such that
A14: g in dom(h|X) and
A15: (h|X).g=r by FUNCT_1:def 3;
A16: h.g=r by A14,A15,FUNCT_1:47;
g in dom h /\ X by A14,RELAT_1:61;
then
A17: g in dom h by XBOOLE_0:def 4;
((hX)").r<>(h").r by A10,A11,A12,FUNCT_1:47;
then g<>(h").(h.t) by A14,A15,A13,FUNCT_1:34;
hence contradiction by A13,A17,A16,FUNCT_1:34;
end;
hence thesis by A10;
end;
theorem Th18:
for h being PartFunc of W,REAL holds
rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h)
implies h is constant
proof
let h be PartFunc of W,REAL;
assume
A1: rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h);
assume not h is constant;
then consider x1,x2 being object such that
A2: x1 in dom h & x2 in dom h and
A3: h.x1 <> h.x2;
h.x1 in rng h & h.x2 in rng h by A2,FUNCT_1:def 3;
hence contradiction by A1,A3,SEQ_4:12;
end;
theorem
for h being PartFunc of W,REAL holds
h.:Y is real-bounded & upper_bound(h.:Y) = lower_bound(h.:Y) implies
h|Y is constant
proof
let h be PartFunc of W,REAL;
rng (h|Y) = h.:Y by RELAT_1:115;
hence thesis by Th18;
end;
reserve e1,e2 for ExtReal;
reserve h,h1,h2 for PartFunc of REAL,REAL;
definition
let h;
redefine attr h is increasing means :: redefines increasing (VALUED_0, definition)
for r1,r2 st r1 in dom h & r2 in dom h & r1<r2 holds h.r1 < h.r2;
compatibility;
redefine attr h is decreasing means :: redefines decreasing (VALUED_0, definition)
for r1,r2 st r1 in dom h & r2 in dom h & r1<r2 holds h.r2 < h.r1;
compatibility;
redefine attr h is non-decreasing means :: redefines non-decreasing (VALUED_0, definition)
for r1,r2 st r1 in dom h & r2 in dom h & r1<r2 holds h.r1 <= h.r2;
compatibility
proof
thus h is non-decreasing implies for r1,r2 st r1 in dom h & r2 in dom h &
r1 < r2 holds h.r1 <= h.r2;
assume
A1: for r1,r2 st r1 in dom h & r2 in dom h & r1 < r2 holds h.r1 <= h. r2;
let e1,e2 such that
A2: e1 in dom h & e2 in dom h;
assume e1 <= e2;
then e1 < e2 or e1 = e2 by XXREAL_0:1;
hence thesis by A1,A2;
end;
redefine attr h is non-increasing means :: redefines non-increasing (VALUED_0, definition)
for r1,r2 st r1 in dom h & r2 in dom h & r1<r2 holds h.r2 <= h.r1;
compatibility
proof
thus h is non-increasing implies for r1,r2 st r1 in dom h & r2 in dom h &
r1 < r2 holds h.r1 >= h.r2;
assume
A3: for r1,r2 st r1 in dom h & r2 in dom h & r1 < r2 holds h.r1 >= h. r2;
let e1,e2 such that
A4: e1 in dom h & e2 in dom h;
assume e1 <= e2;
then e1 < e2 or e1 = e2 by XXREAL_0:1;
hence thesis by A3,A4;
end;
end;
theorem Th20:
h|Y is increasing iff for r1,r2 st r1 in Y /\ dom h & r2 in Y /\
dom h & r1<r2 holds h.r1 < h.r2
proof
thus h|Y is increasing implies for r1,r2 st r1 in Y /\ dom h & r2 in Y /\
dom h & r1<r2 holds h.r2 > h.r1
proof
assume
A1: h|Y is increasing;
let r1,r2 such that
A2: r1 in Y /\ dom h and
A3: r2 in Y /\ dom h and
A4: r1<r2;
A5: r2 in dom(h|Y) by A3,RELAT_1:61;
then
A6: (h|Y).r2 = h.r2 by FUNCT_1:47;
A7: r1 in dom(h|Y) by A2,RELAT_1:61;
then (h|Y).r1 = h.r1 by FUNCT_1:47;
hence thesis by A1,A4,A7,A5,A6;
end;
assume
A8: for r1,r2 st r1 in Y /\ dom h & r2 in Y /\ dom h & r1<r2 holds h.r2 >h.r1;
let r1,r2;
assume that
A9: r1 in dom(h|Y) & r2 in dom(h|Y) and
A10: r1<r2;
A11: (h|Y).r1 = h.r1 & (h|Y).r2 = h.r2 by A9,FUNCT_1:47;
r1 in Y /\ dom h & r2 in Y /\ dom h by A9,RELAT_1:61;
hence thesis by A8,A10,A11;
end;
theorem Th21:
h|Y is decreasing iff for r1,r2 st r1 in Y /\ dom h & r2 in Y /\
dom h & r1<r2 holds h.r2 < h.r1
proof
thus h|Y is decreasing implies for r1,r2 st r1 in Y /\ dom h & r2 in Y /\
dom h & r1<r2 holds h.r2 < h.r1
proof
assume
A1: h|Y is decreasing;
let r1,r2 such that
A2: r1 in Y /\ dom h and
A3: r2 in Y /\ dom h and
A4: r1<r2;
A5: r2 in dom(h|Y) by A3,RELAT_1:61;
then
A6: (h|Y).r2 = h.r2 by FUNCT_1:47;
A7: r1 in dom(h|Y) by A2,RELAT_1:61;
then (h|Y).r1 = h.r1 by FUNCT_1:47;
hence thesis by A1,A4,A7,A5,A6;
end;
assume
A8: for r1,r2 st r1 in Y /\ dom h & r2 in Y /\ dom h & r1<r2 holds h.r2 <h.r1;
let r1,r2;
assume that
A9: r1 in dom(h|Y) & r2 in dom(h|Y) and
A10: r1<r2;
A11: (h|Y).r1 = h.r1 & (h|Y).r2 = h.r2 by A9,FUNCT_1:47;
r1 in Y /\ dom h & r2 in Y /\ dom h by A9,RELAT_1:61;
hence thesis by A8,A10,A11;
end;
theorem Th22:
h|Y is non-decreasing iff for r1,r2 st r1 in Y /\ dom h & r2 in
Y /\ dom h & r1<r2 holds h.r1 <= h.r2
proof
thus h|Y is non-decreasing implies for r1,r2 st r1 in Y /\ dom h & r2 in Y
/\ dom h & r1<r2 holds h.r1 <= h.r2
proof
assume
A1: h|Y is non-decreasing;
let r1,r2 such that
A2: r1 in Y /\ dom h and
A3: r2 in Y /\ dom h and
A4: r1<r2;
A5: r2 in dom(h|Y) by A3,RELAT_1:61;
then
A6: (h|Y).r2 = h.r2 by FUNCT_1:47;
A7: r1 in dom(h|Y) by A2,RELAT_1:61;
then (h|Y).r1 = h.r1 by FUNCT_1:47;
hence thesis by A1,A4,A7,A5,A6;
end;
assume
A8: for r1,r2 st r1 in Y /\ dom h & r2 in Y /\ dom h & r1<r2 holds h.r1
<= h.r2;
let r1,r2;
assume that
A9: r1 in dom(h|Y) & r2 in dom(h|Y) and
A10: r1<r2;
A11: (h|Y).r1 = h.r1 & (h|Y).r2 = h.r2 by A9,FUNCT_1:47;
r1 in Y /\ dom h & r2 in Y /\ dom h by A9,RELAT_1:61;
hence thesis by A8,A10,A11;
end;
theorem Th23:
h|Y is non-increasing iff for r1,r2 st r1 in Y /\ dom h & r2 in
Y /\ dom h & r1<r2 holds h.r2 <= h.r1
proof
thus h|Y is non-increasing implies for r1,r2 st r1 in Y /\ dom h & r2 in Y
/\ dom h & r1<r2 holds h.r2 <= h.r1
proof
assume
A1: h|Y is non-increasing;
let r1,r2 such that
A2: r1 in Y /\ dom h and
A3: r2 in Y /\ dom h and
A4: r1<r2;
A5: r2 in dom(h|Y) by A3,RELAT_1:61;
then
A6: (h|Y).r2 = h.r2 by FUNCT_1:47;
A7: r1 in dom(h|Y) by A2,RELAT_1:61;
then (h|Y).r1 = h.r1 by FUNCT_1:47;
hence thesis by A1,A4,A7,A5,A6;
end;
assume
A8: for r1,r2 st r1 in Y /\ dom h & r2 in Y /\ dom h & r1<r2 holds h.r2 <=h.r1;
let r1,r2;
assume that
A9: r1 in dom(h|Y) & r2 in dom(h|Y) and
A10: r1<r2;
A11: (h|Y).r1 = h.r1 & (h|Y).r2 = h.r2 by A9,FUNCT_1:47;
r1 in Y /\ dom h & r2 in Y /\ dom h by A9,RELAT_1:61;
hence thesis by A8,A10,A11;
end;
definition
let h;
attr h is monotone means
h is non-decreasing or h is non-increasing;
end;
registration
cluster non-decreasing -> monotone for PartFunc of REAL,REAL;
coherence;
cluster non-increasing -> monotone for PartFunc of REAL,REAL;
coherence;
cluster non monotone -> non non-decreasing non non-increasing for PartFunc of
REAL,REAL;
coherence;
end;
theorem Th24:
h|Y is non-decreasing iff for r1,r2 st r1 in Y /\ dom h & r2 in Y /\ dom h &
r1 <= r2 holds h.r1 <= h.r2
proof
thus h|Y is non-decreasing implies for r1,r2 st r1 in Y /\ dom h & r2 in Y
/\ dom h & r1<=r2 holds h.r1 <= h.r2
proof
assume
A1: h|Y is non-decreasing;
let r1,r2 such that
A2: r1 in Y /\ dom h & r2 in Y /\ dom h and
A3: r1<=r2;
now
per cases by A3,XXREAL_0:1;
suppose
r1 < r2;
hence thesis by A1,A2,Th22;
end;
suppose
r1 = r2;
hence thesis;
end;
end;
hence thesis;
end;
assume
A4: for r1,r2 st r1 in Y /\ dom h & r2 in Y /\ dom h & r1<=r2 holds h.
r1 <= h.r2;
let r1,r2;
assume that
A5: r1 in dom(h|Y) & r2 in dom(h|Y) and
A6: r1<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 thesis by A4,A6,A7;
end;
theorem Th25:
h|Y is non-increasing iff for r1,r2 st r1 in Y /\ dom h & r2 in
Y /\ dom h & r1<=r2 holds h.r2 <= h.r1
proof
thus h|Y is non-increasing implies for r1,r2 st r1 in Y /\ dom h & r2 in Y
/\ dom h & r1<=r2 holds h.r2 <= h.r1
proof
assume
A1: h|Y is non-increasing;
let r1,r2 such that
A2: r1 in Y /\ dom h & r2 in Y /\ dom h and
A3: r1<=r2;
now
per cases by A3,XXREAL_0:1;
suppose
r1 < r2;
hence thesis by A1,A2,Th23;
end;
suppose
r1 = r2;
hence thesis;
end;
end;
hence thesis;
end;
assume
A4: for r1,r2 st r1 in Y /\ dom h & r2 in Y /\ dom h & r1<=r2 holds h.
r2<=h.r1;
let r1,r2;
assume that
A5: r1 in dom(h|Y) & r2 in dom(h|Y) and
A6: r1<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 thesis by A4,A6,A7;
end;
registration
cluster non-decreasing non-increasing -> constant for PartFunc of REAL,REAL;
coherence
proof
let h be PartFunc of REAL,REAL;
assume
A1: h is non-decreasing non-increasing;
let r1,r2 be object;
assume
A2: r1 in dom h & r2 in dom h;
then reconsider r1,r2 as Real;
r1 < r2 or r1 = r2 or r2 < r1 by XXREAL_0:1;
then h.r1 <= h.r2 & h.r2 <= h.r1 by A1,A2;
hence thesis by XXREAL_0:1;
end;
end;
registration
cluster constant -> non-increasing non-decreasing for PartFunc of REAL,REAL;
coherence;
end;
registration
cluster trivial for PartFunc of REAL,REAL;
existence
proof
reconsider f = {} as PartFunc of REAL,REAL by RELSET_1:12;
take f;
thus thesis;
end;
end;
theorem
Y misses dom h implies h|Y is increasing & h|Y is decreasing &
h|Y is non-decreasing & h|Y is non-increasing & h|Y is monotone
proof
assume
A1: Y /\ dom h = {};
then
for r1,r2 holds ( r1 in Y /\ dom h & r2 in Y /\ dom h & r1<r2 implies h.
r1<h.r2);
hence h|Y is increasing by Th20;
for r1,r2 holds ( r1 in Y /\ dom h & r2 in Y /\ dom h & r1<r2 implies h.
r2<h.r1) by A1;
hence h|Y is decreasing by Th21;
for r1,r2 holds ( r1 in Y /\ dom h & r2 in Y /\ dom h & r1<r2 implies h.
r1<= h.r2) by A1;
hence h|Y is non-decreasing by Th22;
A2: for r1,r2 holds ( r1 in Y /\ dom h & r2 in Y /\ dom h & r1<r2 implies h.
r2<= h.r1) by A1;
hence h|Y is non-increasing by Th23;
thus thesis by A2,Th23;
end;
theorem
h|Y is non-decreasing & h|X is non-increasing implies h|(Y /\ X) is constant
proof
assume
A1: h|Y is non-decreasing & h|X is non-increasing;
per cases;
suppose
Y /\ X /\ dom h = {};
then Y /\ X misses dom h;
hence thesis by PARTFUN2:39;
end;
suppose
A2: Y /\ X /\ dom h <> {};
set x = the Element of Y /\ X /\ dom h;
x in dom h by A2,XBOOLE_0:def 4;
then reconsider x as Element of REAL;
now
reconsider r1 = h.x as Element of REAL by XREAL_0:def 1;
take r1;
now
let p be Element of REAL;
assume
A3: p in Y /\ X /\ dom h;
then
A4: p in Y /\ X by XBOOLE_0:def 4;
A5: p in dom h by A3,XBOOLE_0:def 4;
p in X by A4,XBOOLE_0:def 4;
then
A6: p in (X /\ dom h) by A5,XBOOLE_0:def 4;
A7: x in dom h by A2,XBOOLE_0:def 4;
A8: x in Y /\ X by A2,XBOOLE_0:def 4;
then x in Y by XBOOLE_0:def 4;
then
A9: x in (Y /\ dom h) by A7,XBOOLE_0:def 4;
x in X by A8,XBOOLE_0:def 4;
then
A10: x in (X /\ dom h) by A7,XBOOLE_0:def 4;
p in Y by A4,XBOOLE_0:def 4;
then
A11: p in (Y /\ dom h) by A5,XBOOLE_0:def 4;
per cases;
suppose
x <= p;
then h.x <= h.p & h.p <= h.x by A1,A11,A6,A9,A10,Th24,Th25;
hence h.p = h.x by XXREAL_0:1;
end;
suppose
p <= x;
then h.p <= h.x & h.x <= h.p by A1,A11,A6,A9,A10,Th24,Th25;
hence h.p = h.x by XXREAL_0:1;
end;
end;
hence for p being Element of REAL
st p in Y /\ X /\ dom h holds h.p = r1;
end;
hence thesis by PARTFUN2:57;
end;
end;
theorem
X c= Y & h|Y is increasing implies h|X is increasing
proof
assume that
A1: X c= Y and
A2: h|Y is increasing;
now
A3: X /\ dom h c= Y /\ dom h by A1,XBOOLE_1:26;
let r1,r2;
assume r1 in X /\ dom h & r2 in X /\ dom h & r1 < r2;
hence h.r1 < h.r2 by A2,A3,Th20;
end;
hence thesis by Th20;
end;
theorem
X c= Y & h|Y is decreasing implies h|X is decreasing
proof
assume that
A1: X c= Y and
A2: h|Y is decreasing;
now
A3: X /\ dom h c= Y /\ dom h by A1,XBOOLE_1:26;
let r1,r2;
assume r1 in X /\ dom h & r2 in X /\ dom h & r1 < r2;
hence h.r1 > h.r2 by A2,A3,Th21;
end;
hence thesis by Th21;
end;
theorem
X c= Y & h|Y is non-decreasing implies h|X is non-decreasing
proof
assume that
A1: X c= Y and
A2: h|Y is non-decreasing;
now
A3: X /\ dom h c= Y /\ dom h by A1,XBOOLE_1:26;
let r1,r2;
assume r1 in X /\ dom h & r2 in X /\ dom h & r1 < r2;
hence h.r1 <= h.r2 by A2,A3,Th22;
end;
hence thesis by Th22;
end;
theorem
X c= Y & h|Y is non-increasing implies h|X is non-increasing
proof
assume that
A1: X c= Y and
A2: h|Y is non-increasing;
now
A3: X /\ dom h c= Y /\ dom h by A1,XBOOLE_1:26;
let r1,r2;
assume r1 in X /\ dom h & r2 in X /\ dom h & r1 < r2;
hence h.r1 >= h.r2 by A2,A3,Th23;
end;
hence thesis by Th23;
end;
theorem Th32:
(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
thus h|Y is increasing & 0<r implies (r(#)h)|Y is increasing
proof
assume that
A1: h|Y is increasing and
A2: 0<r;
now
let r1,r2;
assume that
A3: r1 in Y /\ dom (r(#)h) and
A4: r2 in Y /\ dom (r(#) h) and
A5: r1<r2;
A6: 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,Th20;
then r* h.r1 < r* h.r2 by A2,XREAL_1:68;
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;
end;
hence thesis by Th20;
end;
thus r = 0 implies (r(#)h)|Y is constant
proof
assume
A11: r = 0;
A12: 0 in REAL by XREAL_0:def 1;
now
let r1 be Element of REAL;
assume r1 in Y /\ dom (r(#)h);
then
A13: r1 in dom (r(#)h) by XBOOLE_0:def 4;
r* h.r1 = 0 by A11;
hence (r(#)h).r1 = 0 by A13,VALUED_1:def 5;
end;
hence thesis by PARTFUN2:57,A12;
end;
assume that
A14: h|Y is increasing and
A15: r<0;
now
let r1,r2;
assume that
A16: r1 in Y /\ dom (r(#)h) and
A17: r2 in Y /\ dom (r(#) h) and
A18: r1<r2;
A19: r2 in Y by A17,XBOOLE_0:def 4;
A20: r2 in dom (r(#) h) by A17,XBOOLE_0:def 4;
then r2 in dom h by VALUED_1:def 5;
then
A21: r2 in Y /\ dom h by A19,XBOOLE_0:def 4;
A22: r1 in Y by A16,XBOOLE_0:def 4;
A23: r1 in dom (r(#)h) by A16,XBOOLE_0:def 4;
then r1 in dom h by VALUED_1:def 5;
then r1 in Y /\ dom h by A22,XBOOLE_0:def 4;
then h.r1 < h.r2 by A14,A18,A21,Th20;
then r* h.r2 < r* h.r1 by A15,XREAL_1:69;
then (r(#)h).r2 < r * h.r1 by A20,VALUED_1:def 5;
hence (r(#)h).r2 < (r(#)h).r1 by A23,VALUED_1:def 5;
end;
hence thesis by Th21;
end;
theorem
(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
thus h|Y is decreasing & 0<r implies (r(#)h)|Y is decreasing
proof
assume that
A1: h|Y is decreasing and
A2: 0<r;
now
let r1,r2;
assume that
A3: r1 in Y /\ dom(r(#)h) and
A4: r2 in Y /\ dom(r(#) h) and
A5: r1<r2;
A6: 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.r2 < h.r1 by A1,A5,A8,Th21;
then r * h.r2 < r * h.r1 by A2,XREAL_1:68;
then (r(#)h).r2 < r * h.r1 by A7,VALUED_1:def 5;
hence (r(#)h).r2 < (r(#)h).r1 by A10,VALUED_1:def 5;
end;
hence thesis by Th21;
end;
assume that
A11: h|Y is decreasing and
A12: r<0;
now
let r1,r2;
assume that
A13: r1 in Y /\ dom(r(#)h) and
A14: r2 in Y /\ dom(r(#) h) and
A15: r1<r2;
A16: 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.r2 < h.r1 by A11,A15,A18,Th21;
then r* h.r1 < r* h.r2 by A12,XREAL_1:69;
then (r(#) h).r1 < r* h.r2 by A20,VALUED_1:def 5;
hence (r(#) h).r1 < (r(#) h).r2 by A17,VALUED_1:def 5;
end;
hence thesis by Th20;
end;
theorem Th34:
(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
thus h|Y is non-decreasing & 0<=r implies (r(#)h)|Y is non-decreasing
proof
assume that
A1: h|Y is non-decreasing and
A2: 0<=r;
now
let r1,r2;
assume that
A3: r1 in Y /\ dom(r(#)h) and
A4: r2 in Y /\ dom(r(#) h) and
A5: r1<r2;
A6: 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;
end;
hence thesis by Th22;
end;
assume that
A11: h|Y is non-decreasing and
A12: r<=0;
now
let r1,r2;
assume that
A13: r1 in Y /\ dom (r(#)h) and
A14: r2 in Y /\ dom (r(#) h) and
A15: r1<r2;
A16: 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;
end;
hence thesis by Th23;
end;
theorem
(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
thus h|Y is non-increasing & 0<=r implies (r(#)h)|Y is non-increasing
proof
assume that
A1: h|Y is non-increasing and
A2: 0<=r;
now
let r1,r2;
assume that
A3: r1 in Y /\ dom(r(#)h) and
A4: r2 in Y /\ dom(r(#) h) and
A5: r1<r2;
A6: 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.r2 <= h.r1 by A1,A5,A8,Th23;
then r* h.r2 <= (h.r1)*r by A2,XREAL_1:64;
then (r(#)h).r2 <= r * h.r1 by A7,VALUED_1:def 5;
hence (r(#)h).r2 <= (r(#)h).r1 by A10,VALUED_1:def 5;
end;
hence thesis by Th23;
end;
assume that
A11: h|Y is non-increasing and
A12: r<=0;
now
let r1,r2;
assume that
A13: r1 in Y /\ dom (r(#)h) and
A14: r2 in Y /\ dom (r(#)h) and
A15: r1<r2;
A16: 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.r2 <= h.r1 by A11,A15,A18,Th23;
then r* h.r1 <= r* h.r2 by A12,XREAL_1:65;
then (r(#)h).r1 <= r * h.r2 by A20,VALUED_1:def 5;
hence (r(#)h).r1 <= (r(#)h).r2 by A17,VALUED_1:def 5;
end;
hence thesis by Th22;
end;
theorem Th36:
r in X /\ Y /\ dom (h1+h2) implies r in X /\ dom h1 & r in Y /\ dom h2
proof
assume
A1: r in X /\ Y /\ dom (h1+h2);
then r in dom (h1+h2) by XBOOLE_0:def 4;
then r in dom h1 /\ dom h2 by VALUED_1:def 1;
then
A2: r in dom h1 & r in dom h2 by XBOOLE_0:def 4;
r in X /\ Y by A1,XBOOLE_0:def 4;
then r in X & r in Y by XBOOLE_0:def 4;
hence thesis by A2,XBOOLE_0:def 4;
end;
theorem
(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
thus h1|X is increasing & h2|Y is increasing implies (h1+h2)|(X /\ Y) is
increasing
proof
assume that
A1: h1|X is increasing and
A2: h2|Y is increasing;
now
let r1,r2;
assume that
A3: r1 in X /\ Y /\ dom (h1+h2) and
A4: r2 in X /\ Y /\ dom (h1+h2) and
A5: r1<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;
end;
hence thesis by Th20;
end;
thus h1|X is decreasing & h2|Y is decreasing implies (h1+h2)|(X /\ Y) is
decreasing
proof
assume that
A9: h1|X is decreasing and
A10: h2|Y is decreasing;
now
let r1,r2;
assume that
A11: r1 in X /\ Y /\ dom (h1+h2) and
A12: r2 in X /\ Y /\ dom (h1+h2) and
A13: r1<r2;
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;
end;
hence thesis by Th21;
end;
thus h1|X is non-decreasing & h2|Y is non-decreasing implies (h1+h2)|(X /\ Y
) is non-decreasing
proof
assume that
A17: h1|X is non-decreasing and
A18: h2|Y is non-decreasing;
now
let r1,r2;
assume that
A19: r1 in X /\ Y /\ dom (h1+h2) and
A20: r2 in X /\ Y /\ dom (h1+h2) and
A21: r1<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;
end;
hence thesis by Th22;
end;
assume that
A25: h1|X is non-increasing and
A26: h2|Y is non-increasing;
now
let r1,r2;
assume that
A27: r1 in X /\ Y /\ dom (h1+h2) and
A28: r2 in X /\ Y /\ dom (h1+h2) and
A29: r1<r2;
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;
end;
hence thesis by Th23;
end;
theorem
(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
thus h1|X is increasing & h2|Y is constant implies (h1+h2)|(X /\ Y) is
increasing
proof
assume that
A1: h1|X is increasing and
A2: h2|Y is constant;
consider r being Element of REAL such that
A3: for p being Element of REAL st p in Y /\ dom h2 holds h2.p = r
by A2,PARTFUN2:57;
now
let r1,r2;
assume that
A4: r1 in X /\ Y /\ dom (h1+h2) and
A5: r2 in X /\ Y /\ dom (h1+h2) and
A6: r1<r2;
r1 in X /\ dom h1 & r2 in X /\ dom h1 by A4,A5,Th36;
then h1.r1 < h1.r2 by A1,A6,Th20;
then
A7: h1.r1 + r < h1.r2 + r by XREAL_1:6;
r1 in Y /\ dom h2 by A4,Th36;
then
A8: h1.r1 + h2.r1 < h1.r2 + r by A3,A7;
A9: r1 in dom (h1+h2) by A4,XBOOLE_0:def 4;
r2 in Y /\ dom h2 by A5,Th36;
then h1.r1 + h2.r1 < h1.r2 + h2.r2 by A3,A8;
then
A10: (h1+h2).r1 < h1.r2 + h2.r2 by A9,VALUED_1:def 1;
r2 in dom (h1+h2) by A5,XBOOLE_0:def 4;
hence (h1+h2).r1 < (h1+h2).r2 by A10,VALUED_1:def 1;
end;
hence thesis by Th20;
end;
assume that
A11: h1|X is decreasing and
A12: h2|Y is constant;
consider r being Element of REAL such that
A13: for p being Element of REAL st p in Y /\ dom h2 holds h2.p = r
by A12,PARTFUN2:57;
now
let r1,r2;
assume that
A14: r1 in X /\ Y /\ dom (h1+h2) and
A15: r2 in X /\ Y /\ dom (h1+h2) and
A16: r1<r2;
r1 in X /\ dom h1 & r2 in X /\ dom h1 by A14,A15,Th36;
then h1.r2 < h1.r1 by A11,A16,Th21;
then
A17: h1.r2 + r < h1.r1 + r by XREAL_1:6;
r2 in Y /\ dom h2 by A15,Th36;
then
A18: h1.r2 + h2.r2 < h1.r1 + r by A13,A17;
A19: r2 in dom (h1+h2) by A15,XBOOLE_0:def 4;
r1 in Y /\ dom h2 by A14,Th36;
then h1.r2 + h2.r2 < h1.r1 + h2.r1 by A13,A18;
then
A20: (h1+h2).r2 < h1.r1 + h2.r1 by A19,VALUED_1:def 1;
r1 in dom (h1+h2) by A14,XBOOLE_0:def 4;
hence (h1+h2).r2 < (h1+h2).r1 by A20,VALUED_1:def 1;
end;
hence thesis by Th21;
end;
theorem
h1|X is increasing & h2|Y is non-decreasing implies (h1+h2)|(X /\ Y)
is increasing
proof
assume that
A1: h1|X is increasing and
A2: h2|Y is non-decreasing;
now
let r1,r2;
assume that
A3: r1 in X /\ Y /\ dom (h1+h2) and
A4: r2 in X /\ Y /\ dom (h1+h2) and
A5: r1<r2;
A6: r2 in X /\ Y by A4,XBOOLE_0:def 4;
then
A7: r2 in Y by XBOOLE_0:def 4;
A8: r2 in dom (h1+h2) by A4,XBOOLE_0:def 4;
then
A9: r2 in dom h1 /\ dom h2 by VALUED_1:def 1;
then r2 in dom h2 by XBOOLE_0:def 4;
then
A10: r2 in Y /\ dom h2 by A7,XBOOLE_0:def 4;
A11: r1 in X /\ Y by A3,XBOOLE_0:def 4;
then
A12: r1 in Y by XBOOLE_0:def 4;
A13: r1 in dom (h1+h2) by A3,XBOOLE_0:def 4;
then
A14: r1 in dom h1 /\ dom h2 by VALUED_1:def 1;
then r1 in dom h2 by XBOOLE_0:def 4;
then r1 in Y /\ dom h2 by A12,XBOOLE_0:def 4;
then
A15: h2.r1 <= h2.r2 by A2,A5,A10,Th22;
A16: r2 in X by A6,XBOOLE_0:def 4;
A17: r1 in X by A11,XBOOLE_0:def 4;
r2 in dom h1 by A9,XBOOLE_0:def 4;
then
A18: r2 in X /\ dom h1 by A16,XBOOLE_0:def 4;
r1 in dom h1 by A14,XBOOLE_0:def 4;
then r1 in X /\ dom h1 by A17,XBOOLE_0:def 4;
then h1.r1 < h1.r2 by A1,A5,A18,Th20;
then h1.r1 + h2.r1 < h1.r2 + h2.r2 by A15,XREAL_1:8;
then (h1+h2).r1 < h1.r2 + h2.r2 by A13,VALUED_1:def 1;
hence (h1+h2).r1 < (h1+h2).r2 by A8,VALUED_1:def 1;
end;
hence thesis by Th20;
end;
theorem
h1|X is non-increasing & h2|Y is constant implies (h1+h2)|(X /\ Y) is
non-increasing
proof
assume that
A1: h1|X is non-increasing and
A2: h2|Y is constant;
now
let r1,r2;
assume that
A3: r1 in X /\ Y /\ dom (h1+h2) and
A4: r2 in X /\ Y /\ dom (h1+h2) and
A5: r1<r2;
A6: r2 in X /\ Y by A4,XBOOLE_0:def 4;
then
A7: r2 in X by XBOOLE_0:def 4;
A8: r2 in Y by A6,XBOOLE_0:def 4;
A9: r2 in dom (h1+h2) by A4,XBOOLE_0:def 4;
then
A10: r2 in dom h1 /\ dom h2 by VALUED_1:def 1;
then r2 in dom h2 by XBOOLE_0:def 4;
then
A11: r2 in Y /\ dom h2 by A8,XBOOLE_0:def 4;
r2 in dom h1 by A10,XBOOLE_0:def 4;
then
A12: r2 in X /\ dom h1 by A7,XBOOLE_0:def 4;
A13: r1 in X /\ Y by A3,XBOOLE_0:def 4;
then
A14: r1 in X by XBOOLE_0:def 4;
A15: r1 in Y by A13,XBOOLE_0:def 4;
A16: r1 in dom (h1+h2) by A3,XBOOLE_0:def 4;
then
A17: r1 in dom h1 /\ dom h2 by VALUED_1:def 1;
then r1 in dom h2 by XBOOLE_0:def 4;
then r1 in Y /\ dom h2 by A15,XBOOLE_0:def 4;
then
A18: h2.r2 = h2.r1 by A2,A11,PARTFUN2:58;
r1 in dom h1 by A17,XBOOLE_0:def 4;
then r1 in X /\ dom h1 by A14,XBOOLE_0:def 4;
then h1.r2 <= h1.r1 by A1,A5,A12,Th23;
then h1.r2 + h2.r2 <= h1.r1 + h2.r1 by A18,XREAL_1:6;
then (h1+h2).r2 <= h1.r1 + h2.r1 by A9,VALUED_1:def 1;
hence (h1+h2).r2 <= (h1+h2).r1 by A16,VALUED_1:def 1;
end;
hence thesis by Th23;
end;
theorem
h1|X is decreasing & h2|Y is non-increasing implies (h1+h2)|(X /\ Y)
is decreasing
proof
assume that
A1: h1|X is decreasing and
A2: h2|Y is non-increasing;
now
let r1,r2;
assume that
A3: r1 in X /\ Y /\ dom (h1+h2) and
A4: r2 in X /\ Y /\ dom (h1+h2) and
A5: r1<r2;
A6: r2 in X /\ Y by A4,XBOOLE_0:def 4;
then
A7: r2 in Y by XBOOLE_0:def 4;
A8: r2 in dom (h1+h2) by A4,XBOOLE_0:def 4;
then
A9: r2 in dom h1 /\ dom h2 by VALUED_1:def 1;
then r2 in dom h2 by XBOOLE_0:def 4;
then
A10: r2 in Y /\ dom h2 by A7,XBOOLE_0:def 4;
A11: r1 in X /\ Y by A3,XBOOLE_0:def 4;
then
A12: r1 in Y by XBOOLE_0:def 4;
A13: r1 in dom (h1+h2) by A3,XBOOLE_0:def 4;
then
A14: r1 in dom h1 /\ dom h2 by VALUED_1:def 1;
then r1 in dom h2 by XBOOLE_0:def 4;
then r1 in Y /\ dom h2 by A12,XBOOLE_0:def 4;
then
A15: h2.r2 <= h2.r1 by A2,A5,A10,Th23;
A16: r2 in X by A6,XBOOLE_0:def 4;
A17: r1 in X by A11,XBOOLE_0:def 4;
r2 in dom h1 by A9,XBOOLE_0:def 4;
then
A18: r2 in X /\ dom h1 by A16,XBOOLE_0:def 4;
r1 in dom h1 by A14,XBOOLE_0:def 4;
then r1 in X /\ dom h1 by A17,XBOOLE_0:def 4;
then h1.r2 < h1.r1 by A1,A5,A18,Th21;
then h1.r2 + h2.r2 < h1.r1 + h2.r1 by A15,XREAL_1:8;
then (h1+h2).r2 < h1.r1 + h2.r1 by A8,VALUED_1:def 1;
hence (h1+h2).r2 < (h1+h2).r1 by A13,VALUED_1:def 1;
end;
hence thesis by Th21;
end;
theorem
h1|X is non-decreasing & h2|Y is constant implies (h1+h2)|(X /\ Y) is
non-decreasing
proof
assume that
A1: h1|X is non-decreasing and
A2: h2|Y is constant;
now
let r1,r2;
assume that
A3: r1 in X /\ Y /\ dom (h1+h2) and
A4: r2 in X /\ Y /\ dom (h1+h2) and
A5: r1<r2;
A6: r2 in X /\ Y by A4,XBOOLE_0:def 4;
then
A7: r2 in X by XBOOLE_0:def 4;
A8: r2 in Y by A6,XBOOLE_0:def 4;
A9: r2 in dom (h1+h2) by A4,XBOOLE_0:def 4;
then
A10: r2 in dom h1 /\ dom h2 by VALUED_1:def 1;
then r2 in dom h2 by XBOOLE_0:def 4;
then
A11: r2 in Y /\ dom h2 by A8,XBOOLE_0:def 4;
r2 in dom h1 by A10,XBOOLE_0:def 4;
then
A12: r2 in X /\ dom h1 by A7,XBOOLE_0:def 4;
A13: r1 in X /\ Y by A3,XBOOLE_0:def 4;
then
A14: r1 in X by XBOOLE_0:def 4;
A15: r1 in Y by A13,XBOOLE_0:def 4;
A16: r1 in dom (h1+h2) by A3,XBOOLE_0:def 4;
then
A17: r1 in dom h1 /\ dom h2 by VALUED_1:def 1;
then r1 in dom h2 by XBOOLE_0:def 4;
then r1 in Y /\ dom h2 by A15,XBOOLE_0:def 4;
then
A18: h2.r2 = h2.r1 by A2,A11,PARTFUN2:58;
r1 in dom h1 by A17,XBOOLE_0:def 4;
then r1 in X /\ dom h1 by A14,XBOOLE_0:def 4;
then h1.r1 <= h1.r2 by A1,A5,A12,Th22;
then h1.r1 + h2.r1 <= h1.r2 + h2.r2 by A18,XREAL_1:6;
then (h1+h2).r1 <= h1.r2 + h2.r2 by A16,VALUED_1:def 1;
hence (h1+h2).r1 <= (h1+h2).r2 by A9,VALUED_1:def 1;
end;
hence thesis by Th22;
end;
theorem
h|{x} is non-increasing
proof
now
let r1,r2;
assume that
A1: r1 in {x} /\ dom h and
A2: r2 in {x} /\ dom h and
r1<r2;
r1 in {x} by A1,XBOOLE_0:def 4;
then
A3: r1 = x by TARSKI:def 1;
r2 in {x} by A2,XBOOLE_0:def 4;
hence h.r1 >= h.r2 by A3,TARSKI:def 1;
end;
hence thesis by Th23;
end;
theorem
h|{x} is decreasing
proof
now
let r1,r2;
assume that
A1: r1 in {x} /\ dom h and
A2: r2 in {x} /\ dom h and
A3: r1<r2;
r1 in {x} by A1,XBOOLE_0:def 4;
then
A4: r1 = x by TARSKI:def 1;
r2 in {x} by A2,XBOOLE_0:def 4;
hence h.r1 > h.r2 by A3,A4,TARSKI:def 1;
end;
hence thesis by Th21;
end;
theorem
h|{x} is non-decreasing
proof
now
let r1,r2;
assume that
A1: r1 in {x} /\ dom h and
A2: r2 in {x} /\ dom h and
r1<r2;
r1 in {x} by A1,XBOOLE_0:def 4;
then
A3: r1 = x by TARSKI:def 1;
r2 in {x} by A2,XBOOLE_0:def 4;
hence h.r1 <= h.r2 by A3,TARSKI:def 1;
end;
hence thesis by Th22;
end;
theorem
h|{x} is non-increasing
proof
now
let r1,r2;
assume that
A1: r1 in {x} /\ dom h and
A2: r2 in {x} /\ dom h and
r1<r2;
r1 in {x} by A1,XBOOLE_0:def 4;
then
A3: r1 = x by TARSKI:def 1;
r2 in {x} by A2,XBOOLE_0:def 4;
hence h.r2 <= h.r1 by A3,TARSKI:def 1;
end;
hence thesis by Th23;
end;
theorem
(id R)|R is increasing
proof
now
let r1,r2;
assume that
A1: r1 in R /\ dom (id R) and
A2: r2 in R /\ dom (id R) and
A3: r1<r2;
r1 in R by A1,XBOOLE_0:def 4;
then
A4: (id R).r1 = r1 by FUNCT_1:18;
r2 in R by A2,XBOOLE_0:def 4;
hence (id R).r1 < (id R).r2 by A3,A4,FUNCT_1:18;
end;
hence thesis by Th20;
end;
theorem
h|X is increasing implies (-h)|X is decreasing
by Th32;
theorem
h|X is non-decreasing implies (-h)|X is non-increasing
by Th34;
theorem
(h|[.p,g.] is increasing or h|[.p,g.] is decreasing) implies h|[.p,g.]
is one-to-one
proof
assume
A1: h|[.p,g.] is increasing or h|[.p,g.] is decreasing;
now
per cases by A1;
suppose
A2: h|[.p,g.] is increasing;
now
let p1,p2 be Element of REAL;
assume that
A3: p1 in dom(h|[.p,g.]) and
A4: p2 in dom(h|[.p,g.]) and
A5: (h|[.p,g.]).p1 = (h|[.p,g.]).p2;
A6: p1 in [.p,g.] /\ dom h & p2 in [.p,g.] /\ dom h by A3,A4,RELAT_1:61;
A7: h.p1=(h|[.p,g.]).p2 by A3,A5,FUNCT_1:47
.=h.p2 by A4,FUNCT_1:47;
thus p1=p2
proof
assume
A8: p1<>p2;
now
per cases by A8,XXREAL_0:1;
suppose
p1<p2;
hence contradiction by A2,A7,A6,Th20;
end;
suppose
p2<p1;
hence contradiction by A2,A7,A6,Th20;
end;
end;
hence contradiction;
end;
end;
hence thesis;
end;
suppose
A9: h|[.p,g.] is decreasing;
now
let p1,p2 be Element of REAL;
assume that
A10: p1 in dom(h|[.p,g.]) and
A11: p2 in dom(h|[.p,g.]) and
A12: (h|[.p,g.]).p1 = (h|[.p,g.]).p2;
A13: p1 in [.p,g.] /\ dom h & p2 in [.p,g.] /\ dom h by A10,A11,RELAT_1:61;
A14: h.p1=(h|[.p,g.]).p2 by A10,A12,FUNCT_1:47
.=h.p2 by A11,FUNCT_1:47;
thus p1=p2
proof
assume
A15: p1<>p2;
now
per cases by A15,XXREAL_0:1;
suppose
p1<p2;
hence contradiction by A9,A14,A13,Th21;
end;
suppose
p2<p1;
hence contradiction by A9,A14,A13,Th21;
end;
end;
hence contradiction;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
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
let h be one-to-one PartFunc of REAL, REAL;
assume that
A1: h|[.p,g.] is increasing and
A2: (h|[.p,g.])"|(h.:[.p,g.]) is not increasing;
consider y1,y2 be Real such that
A3: y1 in h.:[.p,g.] /\ dom((h|[.p,g.])") and
A4: y2 in h.:[.p,g.] /\ dom((h|[.p,g.])") and
A5: y1<y2 and
A6: ((h|[.p,g.])").y1 >= ((h|[.p,g.])").y2 by A2,Th20;
reconsider yy1 = y1, yy2 = y2 as Real;
y1 in h.:[.p,g.] by A3,XBOOLE_0:def 4;
then
A7: yy1 in rng (h|[.p,g.]) by RELAT_1:115;
y2 in h.:[.p,g.] by A4,XBOOLE_0:def 4;
then
A8: yy2 in rng (h|[.p,g.]) by RELAT_1:115;
A9: h|[.p,g.]|[.p,g.] is increasing by A1;
per cases;
suppose
((h|[.p,g.])").y1 = ((h|[.p,g.])").y2;
then y1 =(h|[.p,g.]).(((h|[.p,g.])").y2) by A7,FUNCT_1:35
.=y2 by A8,FUNCT_1:35;
hence contradiction by A5;
end;
suppose
A10: ((h|[.p,g.])").y1 <> ((h|[.p,g.])").y2;
A11: dom (h|[.p,g.])=dom ((h|[.p,g.])|[.p,g.]) by RELAT_1:72
.=[.p,g.]/\dom(h|[.p,g.]) by RELAT_1:61;
((h|[.p,g.])").yy2 in REAL & ((h|[.p,g.])").yy1 in REAL
by XREAL_0:def 1;
then
A12: ((h|[.p,g.])").yy2 in dom (h|[.p,g.]) & ((h|[.p,g.])").yy1 in dom (h|
[.p,g.]) by A7,A8,PARTFUN2:60;
((h|[.p,g.])").y2 < ((h|[.p,g.])").y1 by A6,A10,XXREAL_0:1;
then (h|[.p,g.]).(((h|[.p,g.])").y2) < (h|[.p,g.]).(((h|[.p,g.])").y1)
by A9,A12,A11,Th20;
then y2 < (h|[.p,g.]).(((h|[.p,g.])").y1) by A8,FUNCT_1:35;
hence contradiction by A5,A7,FUNCT_1:35;
end;
end;
theorem
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
let h be one-to-one PartFunc of REAL, REAL;
assume that
A1: h|[.p,g.] is decreasing and
A2: not (h|[.p,g.])"|(h.:[.p,g.]) is decreasing;
consider y1,y2 be Real such that
A3: y1 in h.:[.p,g.] /\ dom((h|[.p,g.])") and
A4: y2 in h.:[.p,g.] /\ dom((h|[.p,g.])") and
A5: y1<y2 and
A6: ((h|[.p,g.])").y2 >= ((h|[.p,g.])").y1 by A2,Th21;
y1 in h.:[.p,g.] by A3,XBOOLE_0:def 4;
then
A7: y1 in rng (h|[.p,g.]) by RELAT_1:115;
y2 in h.:[.p,g.] by A4,XBOOLE_0:def 4;
then
A8: y2 in rng (h|[.p,g.]) by RELAT_1:115;
A9: h|[.p,g.]|[.p,g.] is decreasing by A1;
now
per cases;
suppose
((h|[.p,g.])").y1 = ((h|[.p,g.])").y2;
then y1 =(h|[.p,g.]).(((h|[.p,g.])").y2) by A7,FUNCT_1:35
.=y2 by A8,FUNCT_1:35;
hence contradiction by A5;
end;
suppose
A10: ((h|[.p,g.])").y1 <> ((h|[.p,g.])").y2;
A11: dom (h|[.p,g.])=dom ((h|[.p,g.])|[.p,g.]) by RELAT_1:72
.=[.p,g.]/\dom(h|[.p,g.]) by RELAT_1:61;
((h|[.p,g.])").y2 in REAL & ((h|[.p,g.])").y1 in REAL &
y1 in REAL & y2 in REAL by XREAL_0:def 1;
then
A12: ((h|[.p,g.])").y2 in dom (h|[.p,g.]) & ((h|[.p,g.])").y1 in dom (h|
[.p,g.]) by A7,A8,PARTFUN2:60;
((h|[.p,g.])").y2 > ((h|[.p,g.])").y1 by A6,A10,XXREAL_0:1;
then (h|[.p,g.]).(((h|[.p,g.])").y2) < (h|[.p,g.]).(((h|[.p,g.])").y1)
by A9,A12,A11,Th21;
then y2 < (h|[.p,g.]).(((h|[.p,g.])").y1) by A8,FUNCT_1:35;
hence contradiction by A5,A7,FUNCT_1:35;
end;
end;
hence contradiction;
end;