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;