:: Monotone Real Sequences. Subsequences :: by Jaros{\l}aw Kotowicz :: :: Received November 23, 1989 :: 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, ARYTM_3, NAT_1, CARD_1, FUNCT_1, XXREAL_0, PARTFUN1, ORDINAL2, RELAT_1, TARSKI, VALUED_0, ARYTM_1, VALUED_1, XXREAL_2, REAL_1, COMPLEX1, FINSEQ_1, SEQM_3, XBOOLE_0, FINSEQ_3, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_3, FINSEQ_1, FINSEQ_3, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, REAL_1, COMPLEX1, NAT_1, VALUED_0; constructors PARTFUN1, FUNCT_3, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1, VALUED_1, SEQ_2, FINSEQ_1, RECDEF_1, RELSET_1, FINSEQ_3, COMSEQ_2; registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, VALUED_0, FUNCT_2, VALUED_1, RFUNCT_1, RELAT_1, NAT_1, FINSEQ_1, CARD_1, INT_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve n,m,k for Nat; reserve r,r1 for Real; reserve f,seq,seq1 for Real_Sequence; reserve x,y for set; :: :: DEFINITIONS OF MONOTONE AND CONSTANT SEQUENCES :: reserve e1,e2 for ExtReal; definition let f be NAT-defined real-valued Function; redefine attr f is increasing means :: SEQM_3:def 1 for m,n st m in dom f & n in dom f & m < n holds f.m < f.n; redefine attr f is decreasing means :: SEQM_3:def 2 for m,n st m in dom f & n in dom f & m < n holds f.m > f.n; redefine attr f is non-decreasing means :: SEQM_3:def 3 for m,n st m in dom f & n in dom f & m <= n holds f.m <= f.n; redefine attr f is non-increasing means :: SEQM_3:def 4 for m,n st m in dom f & n in dom f & m <= n holds f.m >= f.n; end; definition let seq; attr seq is monotone means :: SEQM_3:def 5 seq is non-decreasing or seq is non-increasing; end; theorem :: SEQM_3:1 seq is increasing iff for n,m st n non-decreasing non-increasing for PartFunc of NAT, REAL; cluster non-decreasing non-increasing -> constant for PartFunc of NAT, REAL; end; registration cluster increasing natural-valued for Real_Sequence; end; registration cluster increasing for sequence of NAT; end; reserve Nseq for increasing sequence of NAT; theorem :: SEQM_3:13 seq is sequence of NAT iff for n holds seq.n is Element of NAT; registration let Nseq,k; cluster Nseq ^\ k -> increasing natural-valued for ext-real-valued Function; end; definition let f be Real_Sequence; redefine attr f is increasing means :: SEQM_3:def 6 for n being Nat holds f.n < f.(n+1); redefine attr f is decreasing means :: SEQM_3:def 7 for n being Nat holds f.n > f.(n+1); redefine attr f is non-decreasing means :: SEQM_3:def 8 for n being Nat holds f.n <= f.(n+1); redefine attr f is non-increasing means :: SEQM_3:def 9 for n being Nat holds f.n >= f.(n+1); end; theorem :: SEQM_3:14 for n holds n<=Nseq.n; registration let s be Real_Sequence, k be Nat; cluster s^\k ->real-valued; end; theorem :: SEQM_3:15 (seq+seq1) ^\k=(seq ^\k) + (seq1 ^\k); theorem :: SEQM_3:16 (-seq) ^\k=-(seq ^\k); theorem :: SEQM_3:17 (seq-seq1) ^\k=(seq ^\k)-(seq1 ^\k); theorem :: SEQM_3:18 (seq") ^\k=(seq ^\k)"; theorem :: SEQM_3:19 (seq(#)seq1) ^\k=(seq ^\k)(#)(seq1 ^\k); theorem :: SEQM_3:20 (seq/"seq1) ^\k=(seq ^\k)/"(seq1 ^\k); theorem :: SEQM_3:21 (r(#)seq) ^\k=r(#)(seq ^\k); :: :: SUBSEQUENCES OF MONOTONE SEQUENCE :: SUBSEQUENCE OF BOUNDED SEQUENCE :: theorem :: SEQM_3:22 seq is increasing & seq1 is subsequence of seq implies seq1 is increasing; theorem :: SEQM_3:23 seq is decreasing & seq1 is subsequence of seq implies seq1 is decreasing; theorem :: SEQM_3:24 seq is non-decreasing & seq1 is subsequence of seq implies seq1 is non-decreasing; theorem :: SEQM_3:25 seq is non-increasing & seq1 is subsequence of seq implies seq1 is non-increasing; theorem :: SEQM_3:26 seq is monotone & seq1 is subsequence of seq implies seq1 is monotone; theorem :: SEQM_3:27 seq is bounded_above & seq1 is subsequence of seq implies seq1 is bounded_above; theorem :: SEQM_3:28 seq is bounded_below & seq1 is subsequence of seq implies seq1 is bounded_below; theorem :: SEQM_3:29 seq is bounded & seq1 is subsequence of seq implies seq1 is bounded; :: :: OPERATIONS ON MONOTONE SEQUENCES :: theorem :: SEQM_3:30 (seq is increasing & 0 natural-valued for FinSequence of NAT; end; begin :: moved from GOBOARD1, 2010.03.01, A.T. reserve v for FinSequence of REAL, r,s for Real, n,m,i,j,k for Nat; ::$CT theorem :: SEQM_3:41 |.r-s.|=1 iff r>s & r=s+1 or r1 iff ex m st n=m+1 & m>0; theorem :: SEQM_3:44 for f being FinSequence,n,m,k st len f = m+1 & n in dom f & k in Seg m holds Del(f,n).k = f.k or Del(f,n).k = f.(k+1); definition let f be FinSequence; redefine attr f is constant means :: SEQM_3:def 10 for n,m st n in dom f & m in dom f holds f.n=f.m; end; registration cluster -> real-valued for FinSequence of REAL; end; registration cluster non empty increasing for FinSequence of REAL; end; registration cluster constant for FinSequence of REAL; end; theorem :: SEQM_3:45 v<>{} & rng v c= Seg n & v.(len v) = n & (for k st 1<=k & k<=len v - 1 holds for r,s st r = v.k & s = v.(k+1) holds |.r-s.| = 1 or r=s) & i in Seg n & i+1 in Seg n & m in dom v & v.m = i & (for k st k in dom v & v.k = i holds k<=m) implies m+1 in dom v & v.(m+1)=i+1; theorem :: SEQM_3:46 v<>{} & rng v c= Seg n & v.1 = 1 & v.(len v) = n & (for k st 1<=k & k <=len v - 1 holds for r,s st r = v.k & s = v.(k+1) holds |.r-s.| = 1 or r=s) implies (for i st i in Seg n ex k st k in dom v & v.k = i) & for m,k,i,r st m in dom v & v.m = i & (for j st j in dom v & v.j = i holds j<=m) & m