:: Properties of Real Functions :: by Jaros{\l}aw Kotowicz :: :: Received June 18, 1990 :: Copyright (c) 1990-2021 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