:: Sequences in $R^n$
::  by Agnieszka Sakowicz , Jaros{\l}aw Gryko and Adam Grabowski
::
:: Received May 10, 1994
:: Copyright (c) 1994-2021 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, NAT_1, EUCLID, REAL_1, PRE_TOPC,
      FUNCT_1, RELAT_1, VALUED_0, TARSKI, STRUCT_0, SUPINF_2, ARYTM_3, ARYTM_1,
      COMPLEX1, VALUED_1, CARD_1, XXREAL_0, XXREAL_2, SEQ_2, ORDINAL2,
      XBOOLE_0, PARTFUN1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1,
      VALUED_1, PARTFUN1, COMPLEX1, REAL_1, PRE_TOPC, XXREAL_0, XCMPLX_0,
      XREAL_0, NAT_1, SEQ_1, STRUCT_0, RLVECT_1, VFUNCT_1, EUCLID;
 constructors REAL_1, COMPLEX1, MONOID_0, EUCLID, RELSET_1, BINOP_2, VFUNCT_1;
 registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0,
      MONOID_0, EUCLID, XBOOLE_0, VALUED_1, FUNCT_2, NUMBERS, VALUED_0, NAT_1;
 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 for Nat;
reserve n,m,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,seq9 for Real_Sequence of N;

theorem :: TOPRNS_1:1
  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= NonZero TOP-REAL N;
end;

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

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

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

definition
  let r be Real;
  let N be Nat,seq be Real_Sequence of N;
  func r * seq -> Real_Sequence of N equals
:: TOPRNS_1:def 3
  r(#)seq;
end;

definition
  let N be Nat,seq be Real_Sequence of N;
  func - seq -> Real_Sequence of N equals
:: TOPRNS_1:def 4
  - seq;
end;

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

definition
  let N be Nat,seq be Real_Sequence of N;
  func |.seq.| -> Real_Sequence means
:: TOPRNS_1:def 6

  for n being Nat holds it.n = |.seq.n.|;
end;

theorem :: TOPRNS_1:4
  for N,n be Nat,seq1,seq2 be Real_Sequence of N holds
  (seq1+seq2).n = seq1.n + seq2.n;

theorem :: TOPRNS_1:5
  for N,n be Nat,seq be Real_Sequence of N holds
  (r*seq).n = r*seq.n;

theorem :: TOPRNS_1:6
  for N,n be Nat,seq be Real_Sequence of N holds
  (-seq).n = -seq.n;

theorem :: TOPRNS_1:7
  |.r.|*|.w.| = |.r*w.|;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: TOPRNS_1:23
  |.0.TOP-REAL N.| = 0;

theorem :: TOPRNS_1:24
  |.w.| = 0 implies w = 0.TOP-REAL N;

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

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

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

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

theorem :: TOPRNS_1:29
  |.w1 + w2.| <= |.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 implies |.w1 - w2.| > 0;

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

definition
  let N;
  let IT be Real_Sequence of N;
  attr IT is bounded means
:: TOPRNS_1:def 7

  ex r st for n holds |.IT.n.| < r;
end;

theorem :: TOPRNS_1:35
  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 8

  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 9

  for r st 0<r ex n st for m st n<=m holds |.seq.m-it.| < r;
end;

theorem :: TOPRNS_1:36
  seq is convergent & seq9 is convergent implies seq + seq9 is convergent;

theorem :: TOPRNS_1:37
  seq is convergent & seq9 is convergent implies lim (seq + seq9)=
  (lim seq)+(lim seq9);

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

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

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

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

theorem :: TOPRNS_1:42
  seq is convergent & seq9 is convergent implies seq - seq9 is convergent;

theorem :: TOPRNS_1:43
  seq is convergent & seq9 is convergent implies
  lim(seq - seq9) = (lim seq)-(lim seq9);

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

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