Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### Sequences in \$\calE^N_\rmT\$

by
Agnieszka Sakowicz,
Jaroslaw Gryko, and

MML identifier: TOPRNS_1
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, PRE_TOPC, EUCLID, SEQ_1, RELAT_1, ANPROJ_1, BOOLE,
ARYTM_1, COMPLEX1, FINSEQ_1, ABSVALUE, LATTICES, SEQ_2, ORDINAL2,
ARYTM_3, NORMSP_1;
notation TARSKI, XBOOLE_0, NUMBERS, XREAL_0, RELAT_1, FUNCT_1, REAL_1, NAT_1,
SEQ_1, ABSVALUE, STRUCT_0, NORMSP_1, FINSEQ_1, FINSEQ_2, EUCLID,
PRE_TOPC;
constructors SEQ_1, ABSVALUE, EUCLID, REAL_1, NAT_1, PARTFUN1, NORMSP_1,
MEMBERED, XBOOLE_0;
clusters STRUCT_0, EUCLID, XREAL_0, RELSET_1, SEQ_1, ARYTM_3, MEMBERED,
ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin

definition let N be Nat;
mode Real_Sequence of N is sequence of TOP-REAL N;
end;

reserve N,n,m,k,n1,n2 for Nat;
reserve q,r,r1,r2 for Real;
reserve x,y for set;
reserve w,w1,w2,g,g1,g2 for Point of TOP-REAL N;
reserve seq,seq1,seq2,seq3,seq' for Real_Sequence of N;

canceled;

theorem :: TOPRNS_1:2
for f being Function holds
f is Real_Sequence of N iff
(dom f=NAT & for n holds f.n is Point of TOP-REAL N);

definition
let N;
let IT be Real_Sequence of N;
attr IT is non-zero means
:: TOPRNS_1:def 1
rng IT c= (the carrier of TOP-REAL N) \ {0.REAL N};
end;

theorem :: TOPRNS_1:3
seq is non-zero iff for x st x in NAT holds seq.x<>0.REAL N;

theorem :: TOPRNS_1:4
seq is non-zero iff for n holds seq.n<>0.REAL N;

theorem :: TOPRNS_1:5
for N,seq,seq1 st (for x st x in NAT holds seq.x=seq1.x) holds seq=seq1;

theorem :: TOPRNS_1:6
for N,seq,seq1 st (for n holds seq.n=seq1.n) holds seq=seq1;

scheme ExTopRealNSeq{N()->Nat, F(Nat)->Point of TOP-REAL N()}:
ex seq being Real_Sequence of N() st for n holds seq.n=F(n);

definition
let N,seq1,seq2;
func seq1 + seq2 -> Real_Sequence of N means
:: TOPRNS_1:def 2
for n holds it.n = seq1.n + seq2.n;
end;

definition
let r,N,seq;
func r*seq -> Real_Sequence of N means
:: TOPRNS_1:def 3
for n holds it.n = r*seq.n;
end;

definition
let N,seq;
func - seq -> Real_Sequence of N means
:: TOPRNS_1:def 4
for n holds it.n = -seq.n;
end;

definition
let N,seq1,seq2;
func seq1-seq2 -> Real_Sequence of N equals
:: TOPRNS_1:def 5
seq1 +- seq2;
end;

definition
let N; let x be Point of TOP-REAL N;
func |.x.|-> Real means
:: TOPRNS_1:def 6
ex y be FinSequence of REAL st x=y & it=|.y.|;
end;

definition
let N,seq;
func |.seq.| -> Real_Sequence means
:: TOPRNS_1:def 7
for n holds it.n=|.seq.n.|;
end;

canceled;

theorem :: TOPRNS_1:8
abs(r)*|.w.| = |.r*w.|;

theorem :: TOPRNS_1:9
|.r*seq.| = abs(r)(#)|.seq.|;

theorem :: TOPRNS_1:10
seq1 + seq2 = seq2 + seq1;

theorem :: TOPRNS_1:11
(seq1 + seq2) + seq3 = seq1 + (seq2 + seq3);

theorem :: TOPRNS_1:12
-seq = (-1)*seq;

theorem :: TOPRNS_1:13
r*(seq1 + seq2) = r*seq1 + r*seq2;

theorem :: TOPRNS_1:14
(r*q)*seq = r*(q*seq);

theorem :: TOPRNS_1:15
r*(seq1 - seq2) = r*seq1 - r*seq2;

theorem :: TOPRNS_1:16
seq1 - (seq2 + seq3) = seq1 - seq2 - seq3;

theorem :: TOPRNS_1:17
1*seq=seq;

theorem :: TOPRNS_1:18
-(-seq) = seq;

theorem :: TOPRNS_1:19
seq1 - (-seq2) = seq1 + seq2;

theorem :: TOPRNS_1:20
seq1 - (seq2 - seq3) = seq1 - seq2 + seq3;

theorem :: TOPRNS_1:21
seq1 + (seq2 - seq3) = seq1 + seq2 - seq3;

theorem :: TOPRNS_1:22
r <> 0 & seq is non-zero implies r*seq is non-zero;

theorem :: TOPRNS_1:23
seq is non-zero implies -seq is non-zero;

theorem :: TOPRNS_1:24
|.0.REAL N.| = 0;

theorem :: TOPRNS_1:25
|.w.| = 0 implies w = 0.REAL N;

theorem :: TOPRNS_1:26
|.w.| >= 0;

theorem :: TOPRNS_1:27
|.-w.| = |.w.|;

theorem :: TOPRNS_1:28
|.w1 - w2.| = |.w2 - w1.|;

theorem :: TOPRNS_1:29
|.w1 - w2.| = 0 iff w1 = w2;

theorem :: TOPRNS_1:30
|.w1 + w2.| <= |.w1.| + |.w2.|;

theorem :: TOPRNS_1:31
|.w1 - w2.| <= |.w1.| + |.w2.|;

theorem :: TOPRNS_1:32
|.w1.| - |.w2.| <= |.w1 + w2.|;

theorem :: TOPRNS_1:33
|.w1.| - |.w2.| <= |.w1 - w2.|;

theorem :: TOPRNS_1:34
w1 <> w2 implies |.w1 - w2.| > 0;

theorem :: TOPRNS_1:35
|.w1 - w2.| <= |.w1 - w.| + |.w - w2.|;

theorem :: TOPRNS_1:36
0<=r1 & |.w1.|<|.w2.| & r1<r2 implies |.w1.|*r1<|.w2.|*r2;

canceled;

theorem :: TOPRNS_1:38
-|.w.|<r & r<|.w.| iff abs(r)<|.w.|;

definition
let N;
let IT be Real_Sequence of N;
attr IT is bounded means
:: TOPRNS_1:def 8
ex r st for n holds |.IT.n.| < r;
end;

theorem :: TOPRNS_1:39
for n ex r st (0<r & for m st m<=n holds |.seq.m.| < r);

definition
let N;
let IT be Real_Sequence of N;
attr IT is convergent means
:: TOPRNS_1:def 9
ex g st for r st 0<r ex n st for m st n<=m holds |.IT.m-g.| < r;
end;

definition
let N,seq;
assume  seq is convergent;
func lim seq -> Point of TOP-REAL N means
:: TOPRNS_1:def 10
for r st 0<r ex n st for m st n<=m holds |.seq.m-it.| < r;
end;

canceled;

theorem :: TOPRNS_1:41
seq is convergent & seq' is convergent implies
seq + seq' is convergent;

theorem :: TOPRNS_1:42
seq is convergent & seq' is convergent implies
lim (seq + seq')=(lim seq)+(lim seq');

theorem :: TOPRNS_1:43
seq is convergent implies r*seq is convergent;

theorem :: TOPRNS_1:44
seq is convergent implies lim(r*seq)=r*(lim seq);

theorem :: TOPRNS_1:45
seq is convergent implies - seq is convergent;

theorem :: TOPRNS_1:46
seq is convergent implies lim(-seq)=-(lim seq);

theorem :: TOPRNS_1:47
seq is convergent & seq' is convergent implies
seq - seq' is convergent;

theorem :: TOPRNS_1:48
seq is convergent & seq' is convergent implies
lim(seq - seq')=(lim seq)-(lim seq');

canceled;

theorem :: TOPRNS_1:50
seq is convergent implies seq is bounded;

theorem :: TOPRNS_1:51
seq is convergent implies ((lim seq) <> 0.REAL N implies
ex n st for m st n<=m holds |.(lim seq).|/2 < |.seq.m.|);

```