Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Monotone Real Sequences. Subsequences

**by****Jaroslaw Kotowicz**- Received November 23, 1989
- MML identifier: SEQM_3

- [ Mizar article, MML identifier index ]

environ vocabulary ARYTM, SEQ_1, PARTFUN1, ORDINAL2, FUNCT_1, PROB_1, RELAT_1, ARYTM_1, SEQ_2, LATTICES, ABSVALUE, SEQM_3, FUNCOP_1; notation TARSKI, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, RELAT_1, PARTFUN1, FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, NAT_1, FUNCOP_1; constructors REAL_1, SEQ_2, ABSVALUE, NAT_1, PARTFUN1, MEMBERED, FUNCOP_1, XBOOLE_0; clusters FUNCT_1, XREAL_0, RELSET_1, SEQ_1, ARYTM_3, MEMBERED, FUNCOP_1, ZFMISC_1, XBOOLE_0, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve n,n1,m,k,k1 for Nat; reserve r,r1,r2 for real number; reserve f,seq,seq1,seq2 for Real_Sequence; reserve x,y for set; :: :: DEFINITIONS OF MONOTONE AND CONSTANT SEQUENCES :: definition let f be PartFunc of NAT, REAL; 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; 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; 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; 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 f be Function; attr f is constant means :: SEQM_3:def 5 for n1,n2 being set st n1 in dom f & n2 in dom f holds f.n1=f.n2; end; definition let seq; redefine attr seq is constant means :: SEQM_3:def 6 ex r st for n holds seq.n=r; end; definition let seq; attr seq is monotone means :: SEQM_3:def 7 seq is non-decreasing or seq is non-increasing; end; canceled 6; theorem :: SEQM_3:7 seq is increasing iff for n,m st n<m holds seq.n<seq.m; theorem :: SEQM_3:8 seq is increasing iff for n,k holds seq.n<seq.(n+1+k); theorem :: SEQM_3:9 seq is decreasing iff for n,k holds seq.(n+1+k)<seq.n; theorem :: SEQM_3:10 seq is decreasing iff for n,m st n<m holds seq.m<seq.n; theorem :: SEQM_3:11 seq is non-decreasing iff for n,k holds seq.n<=seq.(n+k); theorem :: SEQM_3:12 seq is non-decreasing iff for n,m st n<=m holds seq.n<=seq.m; theorem :: SEQM_3:13 seq is non-increasing iff for n,k holds seq.(n+k)<=seq.n; theorem :: SEQM_3:14 seq is non-increasing iff for n,m st n<=m holds seq.m<=seq.n; theorem :: SEQM_3:15 seq is constant iff ex r st rng seq={r}; theorem :: SEQM_3:16 seq is constant iff for n holds seq.n=seq.(n+1); theorem :: SEQM_3:17 seq is constant iff for n,k holds seq.n=seq.(n+k); theorem :: SEQM_3:18 seq is constant iff for n,m holds seq.n=seq.m; :: :: PROPORTIES OF MONOTONE AND CONSTANT SEQUENCES :: theorem :: SEQM_3:19 seq is increasing implies for n st 0<n holds seq.0<seq.n; theorem :: SEQM_3:20 seq is decreasing implies for n st 0<n holds seq.n<seq.0; theorem :: SEQM_3:21 seq is non-decreasing implies for n holds seq.0<=seq.n; theorem :: SEQM_3:22 seq is non-increasing implies for n holds seq.n<=seq.0; theorem :: SEQM_3:23 seq is increasing implies seq is non-decreasing; theorem :: SEQM_3:24 seq is decreasing implies seq is non-increasing; theorem :: SEQM_3:25 seq is constant implies seq is non-decreasing; theorem :: SEQM_3:26 seq is constant implies seq is non-increasing; theorem :: SEQM_3:27 seq is non-decreasing & seq is non-increasing implies seq is constant; :: DEFINITIONS OF INCREASING SEQUENCE OF NATURAL NUMBERS, :: RESTRICTION OF SEQUENCE. definition let IT be Relation; attr IT is natural-yielding means :: SEQM_3:def 8 rng IT c= NAT; end; definition cluster increasing natural-yielding Real_Sequence; end; definition mode Seq_of_Nat is natural-yielding Real_Sequence; end; definition let seq,k; func seq ^\k ->Real_Sequence means :: SEQM_3:def 9 for n holds it.n=seq.(n+k); end; reserve Nseq,Nseq1,Nseq2 for increasing Seq_of_Nat; canceled; theorem :: SEQM_3:29 seq is increasing Seq_of_Nat iff seq is increasing & for n holds seq.n is Nat; canceled; theorem :: SEQM_3:31 for n holds (seq*Nseq).n=seq.(Nseq.n); definition let Nseq,n; redefine func Nseq.n ->Nat; end; definition let Nseq,seq; redefine func seq*Nseq ->Real_Sequence; end; definition let Nseq,Nseq1; redefine func Nseq1*Nseq -> increasing Seq_of_Nat; end; definition let Nseq,k; cluster Nseq ^\k -> increasing natural-yielding; end; :: :: DEFINITION OF SUBSEQUENCE :: definition let seq,seq1; pred seq is_subsequence_of seq1 means :: SEQM_3:def 10 ex Nseq st seq=seq1*Nseq; end; definition let f be Real_Sequence; redefine attr f is increasing means :: SEQM_3:def 11 for n being Nat holds f.n < f.(n+1); redefine attr f is decreasing means :: SEQM_3:def 12 for n being Nat holds f.n > f.(n+1); redefine attr f is non-decreasing means :: SEQM_3:def 13 for n being Nat holds f.n <= f.(n+1); redefine attr f is non-increasing means :: SEQM_3:def 14 for n being Nat holds f.n >= f.(n+1); end; canceled; theorem :: SEQM_3:33 for n holds n<=Nseq.n; theorem :: SEQM_3:34 seq ^\0 =seq; theorem :: SEQM_3:35 (seq ^\k)^\m=(seq ^\m)^\k; theorem :: SEQM_3:36 (seq ^\k)^\m=seq ^\(k+m); theorem :: SEQM_3:37 (seq+seq1) ^\k=(seq ^\k) +(seq1 ^\k); theorem :: SEQM_3:38 (-seq) ^\k=-(seq ^\k); theorem :: SEQM_3:39 (seq-seq1) ^\k=(seq ^\k)-(seq1 ^\k); theorem :: SEQM_3:40 seq is_not_0 implies seq ^\k is_not_0; theorem :: SEQM_3:41 (seq") ^\k=(seq ^\k)"; theorem :: SEQM_3:42 (seq(#)seq1) ^\k=(seq ^\k)(#)(seq1 ^\k); theorem :: SEQM_3:43 (seq/"seq1) ^\k=(seq ^\k)/"(seq1 ^\k); theorem :: SEQM_3:44 (r(#)seq) ^\k=r(#)(seq ^\k); theorem :: SEQM_3:45 (seq*Nseq) ^\k=seq*(Nseq ^\k); theorem :: SEQM_3:46 seq is_subsequence_of seq; theorem :: SEQM_3:47 seq ^\k is_subsequence_of seq; theorem :: SEQM_3:48 seq is_subsequence_of seq1 & seq1 is_subsequence_of seq2 implies seq is_subsequence_of seq2; :: :: SUBSEQUENCES OF MONOTONE SEQUENCE :: SUBSEQUENCE OF BOUND SEQUENCE :: theorem :: SEQM_3:49 seq is increasing & seq1 is_subsequence_of seq implies seq1 is increasing; theorem :: SEQM_3:50 seq is decreasing & seq1 is_subsequence_of seq implies seq1 is decreasing; theorem :: SEQM_3:51 seq is non-decreasing & seq1 is_subsequence_of seq implies seq1 is non-decreasing; theorem :: SEQM_3:52 seq is non-increasing & seq1 is_subsequence_of seq implies seq1 is non-increasing; theorem :: SEQM_3:53 seq is monotone & seq1 is_subsequence_of seq implies seq1 is monotone; theorem :: SEQM_3:54 seq is constant & seq1 is_subsequence_of seq implies seq1 is constant; theorem :: SEQM_3:55 seq is constant & seq1 is_subsequence_of seq implies seq=seq1; theorem :: SEQM_3:56 seq is bounded_above & seq1 is_subsequence_of seq implies seq1 is bounded_above; theorem :: SEQM_3:57 seq is bounded_below & seq1 is_subsequence_of seq implies seq1 is bounded_below; theorem :: SEQM_3:58 seq is bounded & seq1 is_subsequence_of seq implies seq1 is bounded; :: :: OPERATIONS ON MONOTONE SEQUENCES :: theorem :: SEQM_3:59 (seq is increasing & 0<r implies r(#)seq is increasing) & (0=r implies r(#)seq is constant) & (seq is increasing & r<0 implies r(#)seq is decreasing); theorem :: SEQM_3:60 (seq is decreasing & 0<r implies r(#)seq is decreasing) & (seq is decreasing & r<0 implies r(#)seq is increasing); theorem :: SEQM_3:61 (seq is non-decreasing & 0<=r implies r(#)seq is non-decreasing) & (seq is non-decreasing & r<=0 implies r(#)seq is non-increasing); theorem :: SEQM_3:62 (seq is non-increasing & 0<=r implies r(#)seq is non-increasing) & (seq is non-increasing & r<=0 implies r(#)seq is non-decreasing); theorem :: SEQM_3:63 (seq is increasing & seq1 is increasing implies seq+seq1 is increasing) & (seq is decreasing & seq1 is decreasing implies seq+seq1 is decreasing) & (seq is non-decreasing & seq1 is non-decreasing implies seq+seq1 is non-decreasing) & (seq is non-increasing & seq1 is non-increasing implies seq+seq1 is non-increasing); theorem :: SEQM_3:64 (seq is increasing & seq1 is constant implies seq+seq1 is increasing) & (seq is decreasing & seq1 is constant implies seq+seq1 is decreasing) & (seq is non-decreasing & seq1 is constant implies seq+seq1 is non-decreasing) & (seq is non-increasing & seq1 is constant implies seq+seq1 is non-increasing); theorem :: SEQM_3:65 seq is constant implies (for r holds r(#)seq is constant) & -seq is constant & abs seq is constant; theorem :: SEQM_3:66 seq is constant & seq1 is constant implies seq(#)seq1 is constant & seq+seq1 is constant; theorem :: SEQM_3:67 seq is constant & seq1 is constant implies seq-seq1 is constant; :: :: OPERATIONS ON BOUND SEQUENCES :: theorem :: SEQM_3:68 (seq is bounded_above & 0<r implies r(#)seq is bounded_above) & (0=r implies r(#)seq is bounded) & (seq is bounded_above & r<0 implies r(#)seq is bounded_below); theorem :: SEQM_3:69 (seq is bounded_below & 0<r implies r(#)seq is bounded_below) & (seq is bounded_below & r<0 implies r(#)seq is bounded_above); theorem :: SEQM_3:70 seq is bounded implies (for r holds r(#)seq is bounded) & -seq is bounded & abs seq is bounded; theorem :: SEQM_3:71 (seq is bounded_above & seq1 is bounded_above implies seq+seq1 is bounded_above) & (seq is bounded_below & seq1 is bounded_below implies seq+seq1 is bounded_below) & (seq is bounded & seq1 is bounded implies seq+seq1 is bounded); theorem :: SEQM_3:72 seq is bounded & seq1 is bounded implies seq(#)seq1 is bounded & seq-seq1 is bounded; :: :: OPERATIONS ON BOUND & CONSTANT SEQUENCES :: theorem :: SEQM_3:73 seq is constant implies seq is bounded; theorem :: SEQM_3:74 seq is constant implies (for r holds r(#)seq is bounded) & (-seq is bounded) & abs seq is bounded; theorem :: SEQM_3:75 (seq is bounded_above & seq1 is constant implies seq+seq1 is bounded_above) & (seq is bounded_below & seq1 is constant implies seq+seq1 is bounded_below) & (seq is bounded & seq1 is constant implies seq+seq1 is bounded); theorem :: SEQM_3:76 (seq is bounded_above & seq1 is constant implies seq-seq1 is bounded_above) & (seq is bounded_below & seq1 is constant implies seq-seq1 is bounded_below) & (seq is bounded & seq1 is constant implies seq-seq1 is bounded & seq1-seq is bounded & seq(#)seq1 is bounded); :: :: OPERATIONS ON BOUND & MONOTONE SEQUENCES :: theorem :: SEQM_3:77 seq is bounded_above & seq1 is non-increasing implies seq+seq1 is bounded_above; theorem :: SEQM_3:78 seq is bounded_below & seq1 is non-decreasing implies seq+seq1 is bounded_below; theorem :: SEQM_3:79 :: YELLOW_6:1 for X,x being set holds X --> x is constant; definition let X,x be set; cluster X --> x -> constant; end;

Back to top