:: Convergent Sequences and the Limit of Sequences
::  by Jaros{\l}aw Kotowicz
::
:: Received July 4, 1989
:: Copyright (c) 1990-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, XREAL_0, SEQ_1, VALUED_0, FUNCT_1, ARYTM_1,
      ARYTM_3, COMPLEX1, XXREAL_0, CARD_1, RELAT_1, XXREAL_2, NAT_1, ORDINAL2,
      TARSKI, REAL_1, VALUED_1, SEQ_2, COMSEQ_1, XCMPLX_0, SQUARE_1;
 notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1,
      REAL_1, NAT_1, RELAT_1, FUNCT_1, VALUED_0, VALUED_1, FUNCOP_1, SEQ_1,
      XXREAL_0, SQUARE_1, COMSEQ_1, COMSEQ_2;
 constructors XXREAL_0, REAL_1, NAT_1, COMPLEX1, PARTFUN1, VALUED_1, RELSET_1,
      FUNCOP_1, COMSEQ_2, SQUARE_1, SEQ_1;
 registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, XBOOLE_0,
      VALUED_0, VALUED_1, FUNCT_2, NUMBERS, COMSEQ_2, XCMPLX_0, SQUARE_1,
      NAT_1, SEQ_1;
 requirements REAL, NUMERALS, SUBSET, ARITHM;


begin

reserve n,n1,n2,m for Nat,
  r,r1,r2,p,g1,g2,g for Real,
  seq,seq9,seq1 for Real_Sequence,
  y for set;

theorem :: SEQ_2:1
  -g<r & r<g iff |.r.|<g;

theorem :: SEQ_2:2
  g<>0 & r<>0 implies |.g"-r".|=|.g-r.|/(|.g.|*|.r.|);

definition
  let f be real-valued Function;
  attr f is bounded_above means
:: SEQ_2:def 1

  ex r st for y being object st y in dom f holds f.y<r;
  attr f is bounded_below means
:: SEQ_2:def 2

  ex r st for y being object st y in dom f holds r<f.y;
end;

definition
  let seq;
  redefine attr seq is bounded_above means
:: SEQ_2:def 3

  ex r st for n holds seq.n<r;
  redefine attr seq is bounded_below means
:: SEQ_2:def 4

  ex r st for n holds r<seq.n;
end;

registration
  cluster bounded -> bounded_above bounded_below for real-valued Function;
  cluster bounded_above bounded_below -> bounded for real-valued Function;
end;

theorem :: SEQ_2:3
  seq is bounded iff ex r st (0<r & for n holds |.seq.n.|<r);

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

::
::          CONVERGENT REAL SEQUENCES
::           THE LIMIT OF SEQUENCES
::

definition
::$CD
  let seq;
  redefine attr seq is convergent means
:: SEQ_2:def 6

  ex g st for p st 0<p ex n st for m st n<=m holds |.seq.m-g.| < p;
end;

definition
  let seq;
  assume
 seq is convergent;
  func lim seq -> Real means
:: SEQ_2:def 7

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

definition
  let f be real-valued Function;
  redefine attr f is bounded means
:: SEQ_2:def 8
  f is bounded_above bounded_below;
end;

registration
  cluster constant -> convergent for Real_Sequence;
end;

theorem :: SEQ_2:5
  seq is convergent & seq9 is convergent implies seq + seq9 is convergent;

registration
  let seq1,seq2 be convergent Real_Sequence;
  cluster seq1 + seq2 -> convergent for Real_Sequence;
end;

theorem :: SEQ_2:6
  seq is convergent & seq9 is convergent implies
  lim (seq + seq9)=(lim seq)+(lim seq9);

theorem :: SEQ_2:7
  seq is convergent implies r(#)seq is convergent;

registration
  let r be Real;
  let seq be convergent Real_Sequence;
  cluster r(#)seq -> convergent for Real_Sequence;
end;

theorem :: SEQ_2:8
  seq is convergent implies lim(r(#)seq)=r*(lim seq);

theorem :: SEQ_2:9
  seq is convergent implies -seq is convergent;

registration
  let seq be convergent Real_Sequence;
  cluster -seq -> convergent for Real_Sequence;
end;

theorem :: SEQ_2:10
  seq is convergent implies lim(-seq) = -(lim seq);

theorem :: SEQ_2:11
  seq is convergent & seq9 is convergent implies seq - seq9 is convergent;

registration
  let seq1,seq2 be convergent Real_Sequence;
  cluster seq1 - seq2 -> convergent for Real_Sequence;
end;

theorem :: SEQ_2:12
  seq is convergent & seq9 is convergent implies
  lim(seq - seq9)=(lim seq)-(lim seq9);

theorem :: SEQ_2:13
  seq is convergent implies seq is bounded;

registration
  cluster convergent -> bounded for Real_Sequence;
end;

theorem :: SEQ_2:14
  seq is convergent & seq9 is convergent implies seq (#) seq9 is convergent;

registration
  let seq1,seq2 be convergent Real_Sequence;
  cluster seq1 (#) seq2 -> convergent for Real_Sequence;
end;

theorem :: SEQ_2:15
  seq is convergent & seq9 is convergent implies
  lim(seq(#)seq9)=(lim seq)*(lim seq9);

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

theorem :: SEQ_2:17
  seq is convergent & (for n holds 0<=seq.n) implies 0<=lim seq;

theorem :: SEQ_2:18
  seq is convergent & seq9 is convergent &
  (for n holds seq.n<=(seq9.n)) implies (lim seq)<=(lim seq9);

theorem :: SEQ_2:19
  seq is convergent & seq9 is convergent &
  (for n holds seq.n<=(seq1.n) & seq1.n<=seq9.n) & (lim seq)=(lim seq9)
  implies seq1 is convergent;

theorem :: SEQ_2:20
  seq is convergent & seq9 is convergent &
  (for n holds seq.n<=(seq1.n) & seq1.n<=seq9.n) &
  lim seq = lim seq9 implies lim seq1 = lim seq;

theorem :: SEQ_2:21
  seq is convergent & lim seq <> 0 & seq is non-zero implies seq" is convergent
;

theorem :: SEQ_2:22
  seq is convergent & lim seq <> 0 & seq is non-zero
  implies lim seq"=(lim seq)";

theorem :: SEQ_2:23
  seq9 is convergent & seq is convergent & lim seq <> 0
  & seq is non-zero implies seq9/"seq is convergent;

theorem :: SEQ_2:24
  seq9 is convergent & seq is convergent & lim seq <> 0
  & seq is non-zero implies lim(seq9/"seq)=(lim seq9)/(lim seq);

theorem :: SEQ_2:25
  seq is convergent & seq1 is bounded & lim seq=0 implies
  seq(#)seq1 is convergent;

theorem :: SEQ_2:26
  seq is convergent & seq1 is bounded & lim seq=0 implies lim(seq(#)seq1)=0;

:: from COMSEQ_2, 2011.07.10, A.T.

reserve g for Complex;

registration
  let s be convergent Complex_Sequence;
  cluster |.s.| -> convergent for Real_Sequence;
end;

reserve s,s1,s9 for Complex_Sequence;

theorem :: SEQ_2:27
  s is convergent implies lim |.s.| = |.lim s.|;

theorem :: SEQ_2:28
 for s,s9 being convergent Complex_Sequence
  holds lim |.(s + s9).| = |.(lim s)+(lim s9).|;

theorem :: SEQ_2:29
  for s being convergent Complex_Sequence
   holds lim |.(r(#)s).| = |.r.|*|.(lim s).|;

theorem :: SEQ_2:30
  for s being convergent Complex_Sequence
  holds lim |.-s.| = |.lim s.|;

theorem :: SEQ_2:31
    for s,s9 being convergent Complex_Sequence
  holds lim |.s - s9.| = |.(lim s) - (lim s9).|;

theorem :: SEQ_2:32
  for s,s9 being convergent Complex_Sequence
  holds lim |.s(#)s9.| = |.lim s.|*|.lim s9.|;

theorem :: SEQ_2:33
  s is convergent & (lim s)<>0c & s is non-zero implies lim |.s".| = (|.
  lim s.|)";

theorem :: SEQ_2:34
  s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero
  implies lim |.(s9/"s).|=|.(lim s9).|/|.(lim s).|;

theorem :: SEQ_2:35
  s is convergent & s1 is bounded & (lim s)=0c implies lim |.s(#)s1.| = 0;