The abstract of the Mizar article:

Sequences in $\calE^N_\rmT$

by

Agnieszka Sakowicz,

Jaroslaw Gryko, and

Adam Grabowski

Received May 10, 1994

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.|);