:: Properties of Real Functions
:: by Jaros{\l}aw Kotowicz
::
:: Received June 18, 1990
:: Copyright (c) 1990-2016 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
:Def1:
for r1,r2 st r1 in dom h & r2 in dom 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 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: r1h.r1;
let r1,r2;
assume that
A9: r1 in dom(h|Y) & r2 in dom(h|Y) and
A10: r1 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 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;
registration
let h be increasing PartFunc of REAL,REAL, X be set;
cluster h|X -> increasing for PartFunc of REAL,REAL;
coherence
proof
now
let r1,r2;
assume
A1: r1 in dom(h|X) & r2 in dom(h|X);
then
A2: h.r1 = (h|X).r1 & h.r2 = (h|X).r2 by FUNCT_1:47;
assume
A3: r1 < r2;
r1 in dom h & r2 in dom h by A1,RELAT_1:57;
hence (h|X).r1 < (h|X).r2 by A2,A3,Def1;
end;
hence thesis;
end;
end;
registration
let h be decreasing PartFunc of REAL,REAL, X be set;
cluster h|X -> decreasing for PartFunc of REAL,REAL;
coherence
proof
now
let r1,r2;
assume
A1: r1 in dom(h|X) & r2 in dom(h|X);
then
A2: h.r1 = (h|X).r1 & h.r2 = (h|X).r2 by FUNCT_1:47;
assume
A3: r1 < r2;
r1 in dom h & r2 in dom h by A1,RELAT_1:57;
hence (h|X).r1 > (h|X).r2 by A2,A3,Def2;
end;
hence thesis;
end;
end;
registration
let h be non-decreasing PartFunc of REAL,REAL, X be set;
cluster h|X -> non-decreasing for PartFunc of REAL,REAL;
coherence
proof
now
let r1,r2;
assume
A1: r1 in dom(h|X) & r2 in dom(h|X);
then
A2: h.r1 = (h|X).r1 & h.r2 = (h|X).r2 by FUNCT_1:47;
assume
A3: r1 < r2;
r1 in dom h & r2 in dom h by A1,RELAT_1:57;
hence (h|X).r1 <= (h|X).r2 by A2,A3,Def3;
end;
hence 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 {};
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= 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 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
r1p2;
now
per cases by A8,XXREAL_0:1;
suppose
p1p2;
now
per cases by A15,XXREAL_0:1;
suppose
p1= ((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= ((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;