Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Monotone Real Sequences. Subsequences

by
Jaroslaw Kotowicz

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;

```