:: 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;
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 :: RFUNCT_2:1
seq1=seq2-seq3 iff for n holds seq1.n=seq2.n-seq3.n;
theorem :: RFUNCT_2:2
(seq1 + seq2)*Ns = (seq1*Ns) + (seq2*Ns) & (seq1 - seq2)*Ns = (
seq1*Ns) - (seq2*Ns) & (seq1 (#) seq2)*Ns = (seq1*Ns) (#) (seq2*Ns);
theorem :: RFUNCT_2:3
(p(#)seq)*Ns = p(#)(seq*Ns);
theorem :: RFUNCT_2:4
(-seq)*Ns = -(seq*Ns) & (abs(seq))*Ns = abs((seq*Ns));
theorem :: RFUNCT_2:5
(seq*Ns)" = (seq")*Ns;
theorem :: RFUNCT_2:6
(seq1/"seq)*Ns = (seq1*Ns)/"(seq*Ns);
theorem :: RFUNCT_2:7
seq is convergent & (for n holds seq.n<=0) implies lim seq <= 0;
theorem :: RFUNCT_2:8
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);
theorem :: RFUNCT_2:9
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);
theorem :: RFUNCT_2:10
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
;
theorem :: RFUNCT_2:11
for h being PartFunc of W,REAL, seq being sequence of W holds
rng seq c= dom (h^) implies h/*seq is non-zero;
theorem :: RFUNCT_2:12
for h being PartFunc of W,REAL, seq being sequence of W holds
rng seq c= dom (h^) implies (h^)/*seq =(h/*seq)";
theorem :: RFUNCT_2:13
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);
theorem :: RFUNCT_2:14
for h being PartFunc of W,REAL, seq being sequence of W holds
h is total implies (r(#)h)/*seq = r(#)(h/*seq);
theorem :: RFUNCT_2:15
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;
theorem :: RFUNCT_2:16
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)";
::
:: MONOTONE FUNCTIONS
::
registration
let Z be set;
let f be one-to-one Function;
cluster f|Z -> one-to-one;
end;
theorem :: RFUNCT_2:17
for h being one-to-one Function holds (h|X)" = (h")|(h.:X);
theorem :: RFUNCT_2:18
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;
theorem :: RFUNCT_2:19
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;
reserve e1,e2 for ExtReal;
reserve h,h1,h2 for PartFunc of REAL,REAL;
definition
let h;
redefine attr h is increasing means
:: RFUNCT_2:def 1
for r1,r2 st r1 in dom h & r2 in dom h & r1 monotone for PartFunc of REAL,REAL;
cluster non-increasing -> monotone for PartFunc of REAL,REAL;
cluster non monotone -> non non-decreasing non non-increasing for PartFunc of
REAL,REAL;
end;
theorem :: RFUNCT_2:24
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;
theorem :: RFUNCT_2:25
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;
registration
cluster non-decreasing non-increasing -> constant for PartFunc of REAL,REAL;
end;
registration
cluster constant -> non-increasing non-decreasing for PartFunc of REAL,REAL;
end;
registration
cluster trivial for PartFunc of REAL,REAL;
end;
registration
let h be increasing PartFunc of REAL,REAL, X be set;
cluster h|X -> increasing for PartFunc of REAL,REAL;
end;
registration
let h be decreasing PartFunc of REAL,REAL, X be set;
cluster h|X -> decreasing for PartFunc of REAL,REAL;
end;
registration
let h be non-decreasing PartFunc of REAL,REAL, X be set;
cluster h|X -> non-decreasing for PartFunc of REAL,REAL;
end;
theorem :: RFUNCT_2:26
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;
theorem :: RFUNCT_2:27
h|Y is non-decreasing & h|X is non-increasing implies h|(Y /\ X) is constant;
theorem :: RFUNCT_2:28
X c= Y & h|Y is increasing implies h|X is increasing;
theorem :: RFUNCT_2:29
X c= Y & h|Y is decreasing implies h|X is decreasing;
theorem :: RFUNCT_2:30
X c= Y & h|Y is non-decreasing implies h|X is non-decreasing;
theorem :: RFUNCT_2:31
X c= Y & h|Y is non-increasing implies h|X is non-increasing;
theorem :: RFUNCT_2:32
(h|Y is increasing & 0