:: Monotone Real Sequences. Subsequences
:: by Jaros{\l}aw Kotowicz
::
:: Received November 23, 1989
:: Copyright (c) 1990-2016 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, SEQ_2, 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 r~~1 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~~