:: Convergent Real Sequences. Upper and Lower Bound of Sets of Real Numbers
::  by Jaros{\l}aw Kotowicz
::
:: Received November 23, 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, SEQ_1, ORDINAL2, NAT_1, ARYTM_3, XXREAL_0,
      REAL_1, CARD_1, ARYTM_1, MEMBERED, XXREAL_2, COMPLEX1, TARSKI, XBOOLE_0,
      SEQ_2, FUNCT_1, VALUED_0, RELAT_1, FUNCOP_1, VALUED_1, SQUARE_1, SEQM_3,
      SEQ_4, BINOP_1, BINOP_2, FINSEQOP, XCMPLX_0, COMPLSP1, FINSEQ_1,
      ZFMISC_1, FINSEQ_2, CARD_3, RVSUM_1, RCOMP_1, SETFAM_1, METRIC_1,
      FINSET_1, ORDINAL4, PARTFUN1, GOBOARD2, MEMBER_1, FUNCT_7;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, CARD_1, FINSET_1,
      MEMBERED, ORDINAL1, NUMBERS, XXREAL_2, XCMPLX_0, XXREAL_0, XREAL_0,
      SETFAM_1, REAL_1, SQUARE_1, COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, SEQ_1,
      COMSEQ_2, SEQ_2, SEQM_3, FUNCT_2, BINOP_1, BINOP_2, FINSEQ_1, FUNCOP_1,
      NAT_1, VALUED_0, VALUED_1, MEMBER_1, RVSUM_1, FINSEQ_2, RECDEF_1,
      FINSEQOP;
 constructors FUNCOP_1, REAL_1, NAT_1, COMPLEX1, PARTFUN1, SEQ_2, SEQM_3,
      SQUARE_1, VALUED_1, RECDEF_1, XXREAL_2, FINSET_1, RELSET_1, BINOP_1,
      BINOP_2, SETWISEO, FINSEQOP, ZFMISC_1, RVSUM_1, MEMBER_1, COMSEQ_2,
      NUMBERS;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0,
      MEMBERED, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, FUNCOP_1, SEQ_2,
      FINSET_1, BINOP_2, FUNCT_1, FINSEQ_2, SUBSET_1, NAT_1, RELAT_1, FINSEQ_1,
      CARD_1, MEMBER_1, SQUARE_1, RVSUM_1, XCMPLX_0, SEQ_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve n,k,k1,m,m1,n1,n2,l for Nat;
reserve r,r1,r2,p,p1,g,g1,g2,s,s1,s2,t for Real;
reserve seq,seq1,seq2 for Real_Sequence;
reserve Nseq for increasing sequence of NAT;
reserve x for set;
reserve X,Y for Subset of REAL;

theorem :: SEQ_4:1
  for X,Y st for r,p st r in X & p in Y holds r<p ex g st for r,p
  st r in X & p in Y holds r<=g & g<=p;

theorem :: SEQ_4:2
  0<p & (ex r st r in X) & (for r st r in X holds r+p in X) implies
  for g ex r st r in X & g<r;

theorem :: SEQ_4:3
  for r ex n st r<n;

theorem :: SEQ_4:4
  X is real-bounded iff ex s st 0<s & for r st r in X holds |.r.|<s;

definition

  let r;
  redefine func {r} -> Subset of REAL;
end;

theorem :: SEQ_4:5
  for X being real-membered set holds X is non empty bounded_above
implies ex g st (for r st r in X holds r<=g) & for s st 0<s ex r st r in X & g-
  s<r;

theorem :: SEQ_4:6
  for X being real-membered set holds (for r st r in X holds r<=g1
) & (for s st 0<s ex r st (r in X & g1-s<r)) & (for r st r in X holds r<=g2) &
  (for s st 0<s ex r st (r in X & g2-s<r)) implies g1=g2;

theorem :: SEQ_4:7
  for X being real-membered set holds X is non empty bounded_below
implies ex g st (for r st r in X holds g<=r) & for s st 0<s ex r st r in X & r<
  g+s;

theorem :: SEQ_4:8
  for X being real-membered set holds (for r st r in X holds g1<=r
) & (for s st 0<s ex r st (r in X & r<g1+s)) & (for r st r in X holds g2<=r) &
  (for s st 0<s ex r st (r in X & r<g2+s)) implies g1=g2;

definition

  let X be real-membered set;
  assume
 X is non empty bounded_above;
  func upper_bound X -> Real means
:: SEQ_4:def 1

  (for r st r in X holds r<=it) & for s st 0<s ex r st r in X & it-s<r;
end;

definition
  let X be real-membered set;
  assume
 X is non empty bounded_below;
  func lower_bound X -> Real means
:: SEQ_4:def 2

  (for r st r in X holds it<=r) & for s st 0<s ex r st r in X & r<it+s;
end;

registration
  let X be non empty bounded_below real-membered set;
  identify lower_bound X with inf X;
end;

registration
  let X be non empty bounded_above real-membered set;
  identify upper_bound X with sup X;
end;

theorem :: SEQ_4:9
  lower_bound {r} = r & upper_bound {r} = r;

theorem :: SEQ_4:10
  lower_bound {r} = upper_bound {r};

theorem :: SEQ_4:11
  X is real-bounded non empty implies lower_bound X <= upper_bound X;

theorem :: SEQ_4:12
  X is real-bounded non empty implies ((ex r,p st r in X & p in X & p<>r) iff
  lower_bound X < upper_bound X);

::
:: Theorems about the Convergence and the Limit
::

theorem :: SEQ_4:13
  seq is convergent implies abs seq is convergent;

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

theorem :: SEQ_4:14
  seq is convergent implies lim abs seq = |.lim seq.|;

theorem :: SEQ_4:15
  abs seq is convergent & lim abs seq=0 implies seq is convergent & lim seq=0;

theorem :: SEQ_4:16
  seq1 is subsequence of seq & seq is convergent implies seq1 is convergent;

theorem :: SEQ_4:17
  seq1 is subsequence of seq & seq is convergent implies lim seq1= lim seq;

theorem :: SEQ_4:18
  seq is convergent & (ex k st for n st k<=n holds seq1.n=seq.n)
  implies seq1 is convergent;

theorem :: SEQ_4:19
  seq is convergent & (ex k st for n st k<=n holds seq1.n=seq.n) implies
  lim seq=lim seq1;

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

theorem :: SEQ_4:20
  seq is convergent implies lim (seq^\k)=lim seq;

theorem :: SEQ_4:21
  seq^\k is convergent implies seq is convergent;

theorem :: SEQ_4:22
  seq^\k is convergent implies lim seq = lim (seq^\k);

theorem :: SEQ_4:23
  seq is convergent & lim seq<>0 implies ex k st (seq ^\k) is non-zero;

theorem :: SEQ_4:24
  seq is convergent & lim seq<>0 implies ex seq1 st seq1 is subsequence
  of seq & seq1 is non-zero;

theorem :: SEQ_4:25
 seq is constant & (r in rng seq or ex n st seq.n=r ) implies lim seq=r;

theorem :: SEQ_4:26
  seq is constant implies for n holds lim seq=seq.n;

theorem :: SEQ_4:27
  seq is convergent & lim seq<>0 implies
  for seq1 st seq1 is subsequence of seq & seq1 is non-zero
  holds lim (seq1")=(lim seq)";

::$CT 3


theorem :: SEQ_4:31
  (for n holds seq.n=g/(n+r)) implies seq is convergent & lim seq =0;

::$CT 3


theorem :: SEQ_4:35
  0<=r & (for n holds seq.n=g/(n*n+r)) implies seq is convergent & lim seq=0;

registration
  cluster non-decreasing bounded_above -> convergent for Real_Sequence;
end;

registration
  cluster non-increasing bounded_below -> convergent for Real_Sequence;
end;

registration
  cluster monotone bounded -> convergent for Real_Sequence;
end;

theorem :: SEQ_4:36
  seq is monotone & seq is bounded implies seq is convergent;

theorem :: SEQ_4:37
  seq is bounded_above & seq is non-decreasing implies for n holds seq.n
  <=lim seq;

theorem :: SEQ_4:38
  seq is bounded_below & seq is non-increasing implies for n holds lim
  seq <= seq.n;

theorem :: SEQ_4:39
  for seq ex Nseq st seq*Nseq is monotone;

::$N Bolzano-Weierstrass Theorem (1 dimension)
theorem :: SEQ_4:40
  seq is bounded implies ex seq1 st seq1 is subsequence of seq &
  seq1 is convergent;

::$N Cauchy sequence
theorem :: SEQ_4:41 :: Cauchy Theorem
  seq is convergent iff for s st 0<s ex n st for m st n<=m
    holds |.seq.m -seq.n.|<s;

theorem :: SEQ_4:42
  seq is constant & seq1 is convergent implies lim (seq+seq1) =(seq.0) +
lim seq1 & lim (seq-seq1) =(seq.0) - lim seq1 & lim (seq1-seq) =(lim seq1) -seq
  .0 & lim (seq(#)seq1) =(seq.0) * (lim seq1);

begin :: Addenda
:: from PSCOMP_1

theorem :: SEQ_4:43
  for X being non empty real-membered set for t st for s st s in X
  holds s >= t holds lower_bound X >= t;

theorem :: SEQ_4:44
  for X being non empty real-membered set st (for s st s in X holds s >=
r) & for t st for s st s in X holds s >= t holds r >= t holds r = lower_bound X
;

theorem :: SEQ_4:45
  for X being non empty real-membered set, r for t st for s st s
  in X holds s <= t holds upper_bound X <= t;

theorem :: SEQ_4:46
  for X being non empty real-membered set, r st (for s st s in X holds s
  <= r) & for t st for s st s in X holds s <= t holds r <= t holds r =
  upper_bound X;

theorem :: SEQ_4:47
  for X being non empty real-membered set, Y being real-membered set st
  X c= Y & Y is bounded_below holds lower_bound Y <= lower_bound X;

theorem :: SEQ_4:48
  for X being non empty real-membered set, Y being real-membered set st
  X c= Y & Y is bounded_above holds upper_bound X <= upper_bound Y;

:: from CQC_SIM1, 2007.03.15, A.T.

definition
  let A be non empty natural-membered set;
  redefine func min A -> Element of NAT;
end;

begin :: moved from COMPLSP1, 2010.02.25

reserve k,n for Nat,
  r,r9,r1,r2 for Real,
  c,c9,c1,c2,c3 for Element of COMPLEX;

theorem :: SEQ_4:49
  0c is_a_unity_wrt addcomplex;

theorem :: SEQ_4:50
  compcomplex is_an_inverseOp_wrt addcomplex;

theorem :: SEQ_4:51
  addcomplex is having_an_inverseOp;

theorem :: SEQ_4:52
  the_inverseOp_wrt addcomplex = compcomplex;

definition
  redefine func diffcomplex equals
:: SEQ_4:def 3
  addcomplex*(id COMPLEX,compcomplex);
end;

theorem :: SEQ_4:53
  1r is_a_unity_wrt multcomplex;

theorem :: SEQ_4:54
  multcomplex is_distributive_wrt addcomplex;

definition let c be Complex;
  func c multcomplex -> UnOp of COMPLEX equals
:: SEQ_4:def 4
  multcomplex[;](c,id COMPLEX);
end;

theorem :: SEQ_4:55
  (c multcomplex).c9 = c*c9;

theorem :: SEQ_4:56
  c multcomplex is_distributive_wrt addcomplex;

definition
  func abscomplex -> Function of COMPLEX,REAL means
:: SEQ_4:def 5
  for c holds it.c = |.c.|;
end;

reserve z,z1,z2 for FinSequence of COMPLEX;

definition let z1,z2;
  redefine func z1 + z2 -> FinSequence of COMPLEX equals
:: SEQ_4:def 6
  addcomplex.:(z1,z2);
  redefine func z1 - z2 -> FinSequence of COMPLEX equals
:: SEQ_4:def 7
  diffcomplex.:(z1,z2);
end;

definition let z;
  redefine func -z -> FinSequence of COMPLEX equals
:: SEQ_4:def 8
  compcomplex*z;
end;

notation let z;
  let c be Complex;
  synonym c*z for c(#)z;
end;

definition let z;
  let c be Complex;
  redefine func c*z -> FinSequence of COMPLEX equals
:: SEQ_4:def 9
  (c multcomplex)*z;
end;

definition let z;
  redefine func abs z -> FinSequence of REAL equals
:: SEQ_4:def 10
  abscomplex*z;
end;

definition let n;
  func COMPLEX n -> FinSequenceSet of COMPLEX equals
:: SEQ_4:def 11
  n-tuples_on COMPLEX;
end;

registration let n;
  cluster COMPLEX n -> non empty;
end;

reserve x,z,z1,z2,z3 for Element of COMPLEX n,
  A,B for Subset of COMPLEX n;

theorem :: SEQ_4:57
  k in Seg n implies z.k in COMPLEX;

definition let n,z1,z2;
  redefine func z1 + z2 -> Element of COMPLEX n;
end;

theorem :: SEQ_4:58
  k in Seg n & c1 = z1.k & c2 = z2.k implies (z1 + z2).k = c1 + c2;

definition let n;
  func 0c n -> FinSequence of COMPLEX equals
:: SEQ_4:def 12
  n |-> 0c;
end;

definition let n;
  redefine func 0c n -> Element of COMPLEX n;
end;

theorem :: SEQ_4:59
  z + 0c n = z & z = 0c n + z;

definition let n,z;
  redefine func -z -> Element of COMPLEX n;
end;

theorem :: SEQ_4:60
  k in Seg n & c = z.k implies (-z).k = -c;

theorem :: SEQ_4:61
  z + -z = 0c n & -z + z = 0c n;

theorem :: SEQ_4:62
  z1 + z2 = 0c n implies z1 = -z2 & z2 = -z1
;

::$CT

theorem :: SEQ_4:64
  -z1 = -z2 implies z1 = z2;

theorem :: SEQ_4:65
  z1 + z = z2 + z or z1 + z = z + z2 implies z1 = z2;

theorem :: SEQ_4:66
  -(z1 + z2) = -z1 + -z2;

definition let n,z1,z2;
  redefine func z1 - z2 -> Element of COMPLEX n;
end;

theorem :: SEQ_4:67
  k in Seg n implies (z1 - z2).k = z1.k - z2.k;

theorem :: SEQ_4:68
  z - 0c n = z;

theorem :: SEQ_4:69
  0c n - z = -z;

theorem :: SEQ_4:70
  z1 - -z2 = z1 + z2;

theorem :: SEQ_4:71
  -(z1 - z2) = z2 - z1;

theorem :: SEQ_4:72
  -(z1 - z2) = -z1 + z2;

theorem :: SEQ_4:73
  z - z = 0c n;

theorem :: SEQ_4:74
  z1 - z2 = 0c n implies z1 = z2;

theorem :: SEQ_4:75
  z1 - z2 - z3 = z1 - (z2 + z3);

theorem :: SEQ_4:76
  z1 + (z2 - z3) = z1 + z2 - z3;

theorem :: SEQ_4:77
  z1 - (z2 - z3) = z1 - z2 + z3;

theorem :: SEQ_4:78
  z1 - z2 + z3 = z1 + z3 - z2;

theorem :: SEQ_4:79
  z1 = z1 + z - z;

theorem :: SEQ_4:80
  z1 + (z2 - z1) = z2;

theorem :: SEQ_4:81
  z1 = z1 - z + z;

definition let n,z,c;
  redefine func c*z -> Element of COMPLEX n;
end;

theorem :: SEQ_4:82
  k in Seg n & c9 = z.k implies (c*z).k = c*c9;

theorem :: SEQ_4:83
  c1*(c2*z) = (c1*c2)*z;

theorem :: SEQ_4:84
  (c1 + c2)*z = c1*z + c2*z;

theorem :: SEQ_4:85
  c*(z1+z2) = c*z1 + c*z2;

theorem :: SEQ_4:86
  1r*z = z;

theorem :: SEQ_4:87
  0c*z = 0c n;

theorem :: SEQ_4:88
  (-1r)*z = -z;

definition let n,z;
  redefine func abs z -> Element of n-tuples_on REAL;
end;

theorem :: SEQ_4:89
  k in Seg n & c = z.k implies (abs z).k = |.c.|;

theorem :: SEQ_4:90
  abs 0c n = n |-> 0;

theorem :: SEQ_4:91
  abs -z = abs z;

theorem :: SEQ_4:92
  abs(c*z) = |.c.|*(abs z);

definition
  let z be FinSequence of COMPLEX;
  func |.z.| -> Real equals
:: SEQ_4:def 13
  sqrt Sum sqr abs z;
end;

theorem :: SEQ_4:93
  |.0c n.| = 0;

theorem :: SEQ_4:94
  |.z.| = 0 implies z = 0c n;

theorem :: SEQ_4:95
  0 <= |.z.|;

theorem :: SEQ_4:96
  |.-z.| = |.z.|;

theorem :: SEQ_4:97
  |.c*z.| = |.c.|*|.z.|;

theorem :: SEQ_4:98
  |.z1 + z2.| <= |.z1.| + |.z2.|;

theorem :: SEQ_4:99
  |.z1 - z2.| <= |.z1.| + |.z2.|;

theorem :: SEQ_4:100
  |.z1.| - |.z2.| <= |.z1 + z2.|;

theorem :: SEQ_4:101
  |.z1.| - |.z2.| <= |.z1 - z2.|;

theorem :: SEQ_4:102
  |.z1 - z2.| = 0 iff z1 = z2;

theorem :: SEQ_4:103
  z1 <> z2 implies 0 < |.z1 - z2.|;

theorem :: SEQ_4:104
  |.z1 - z2.| = |.z2 - z1.|;

theorem :: SEQ_4:105
  |.z1 - z2.| <= |.z1 - z.| + |.z - z2.|;

definition
  let n;
  let A be Subset of COMPLEX n;
  attr A is open means
:: SEQ_4:def 14

  for x st x in A ex r st 0 < r & for z st |.z.| < r holds x + z in A;
end;

definition let n;
  let A be Subset of COMPLEX n;
  attr A is closed means
:: SEQ_4:def 15
  for x st for r st r > 0 ex z st |.z.| < r & x + z in A holds x in A;
end;

theorem :: SEQ_4:106
  for A being Subset of COMPLEX n st A = {} holds A is open;

theorem :: SEQ_4:107
  for A being Subset of COMPLEX n st A = COMPLEX n holds A is open;

theorem :: SEQ_4:108
  for AA being Subset-Family of COMPLEX n st for A being Subset of
  COMPLEX n st A in AA holds A is open for A being Subset of COMPLEX n st A =
  union AA holds A is open;

theorem :: SEQ_4:109
  for A,B being Subset of COMPLEX n st A is open & B is open for C
  being Subset of COMPLEX n st C = A /\ B holds C is open;

definition
  let n,x,r;
  func Ball(x,r) -> Subset of COMPLEX n equals
:: SEQ_4:def 16
  { z : |.z - x.| < r };
end;

theorem :: SEQ_4:110
  z in Ball(x,r) iff |.x - z.| < r;

theorem :: SEQ_4:111
  0 < r implies x in Ball(x,r);

theorem :: SEQ_4:112
  Ball(z1,r1) is open;

definition let n,x,A;
  func dist(x,A) -> Real means
:: SEQ_4:def 17

  for X being Subset of REAL st X = {|.x
  - z.| : z in A} holds it = lower_bound X;
end;

definition let n,A,r;
  func Ball(A,r) -> Subset of COMPLEX n equals
:: SEQ_4:def 18
  { z : dist(z,A) < r };
end;

theorem :: SEQ_4:113
  for X being Subset of REAL, r st X <> {} & for r9 st r9 in X
  holds r <= r9 holds lower_bound X >= r;

theorem :: SEQ_4:114
  A <> {} implies dist(x,A) >= 0;

theorem :: SEQ_4:115
  A <> {} implies dist(x + z,A) <= dist(x,A) + |.z.|;

theorem :: SEQ_4:116
  x in A implies dist(x,A) = 0;

theorem :: SEQ_4:117
  not x in A & A <> {} & A is closed implies dist(x,A) > 0;

theorem :: SEQ_4:118
  A <> {} implies |.z1 - x.| + dist(x,A) >= dist(z1,A);

theorem :: SEQ_4:119
  z in Ball(A,r) iff dist(z,A) < r;

theorem :: SEQ_4:120
  0 < r & x in A implies x in Ball(A,r);

theorem :: SEQ_4:121
  0 < r implies A c= Ball(A,r);

theorem :: SEQ_4:122
  A <> {} implies Ball(A,r1) is open;

definition
  let n,A,B;
  func dist(A,B) -> Real means
:: SEQ_4:def 19

  for X being Subset of REAL st X = {|.x
  - z.| : x in A & z in B} holds it = lower_bound X;
end;

theorem :: SEQ_4:123
  for X,Y being Subset of REAL holds X <> {} & Y <> {} implies X ++ Y <> {};

theorem :: SEQ_4:124
  for X,Y being Subset of REAL holds X is bounded_below &
    Y is bounded_below implies X++Y is bounded_below;

theorem :: SEQ_4:125
  for X,Y being Subset of REAL st
  X <> {} & X is bounded_below & Y <> {} & Y is bounded_below holds
  lower_bound (X ++ Y) = lower_bound X + lower_bound Y;

theorem :: SEQ_4:126
  for X,Y being Subset of REAL st Y is bounded_below & X <> {} &
  for r st r in X ex r1 st r1 in Y & r1 <= r holds
    lower_bound X >= lower_bound Y;

theorem :: SEQ_4:127
  A <> {} & B <> {} implies dist(A,B) >= 0;

theorem :: SEQ_4:128
  dist(A,B) = dist(B,A);

theorem :: SEQ_4:129
  A <> {} & B <> {} implies dist(x,A) + dist(x,B) >= dist(A,B);

theorem :: SEQ_4:130
  A meets B implies dist(A,B) = 0;

definition
  let n;
  func ComplexOpenSets(n) -> Subset-Family of COMPLEX n equals
:: SEQ_4:def 20
  {A where A is
  Subset of COMPLEX n: A is open};
end;

theorem :: SEQ_4:131
  for A being Subset of COMPLEX n holds A in ComplexOpenSets n iff A is open;

theorem :: SEQ_4:132
  for A being Subset of COMPLEX n holds A is closed iff A` is open;

begin :: moved from GOBOARD2, 2010.03.01, A.T.

reserve
  v,v1,v2 for FinSequence of REAL,
  n,m,k for Nat,
  x for set;

theorem :: SEQ_4:133
  for R being finite Subset of REAL holds R <> {} implies R is
bounded_above & upper_bound(R) in R & R is bounded_below & lower_bound(R) in R;

theorem :: SEQ_4:134
  for n being Nat for f being FinSequence holds 1 <= n & n+1 <= len
  f iff n in dom f & n+1 in dom f;

theorem :: SEQ_4:135
  for n being Nat for f being FinSequence holds 1 <= n & n+2 <= len f
  iff n in dom f & n+1 in dom f & n+2 in dom f;

theorem :: SEQ_4:136
  for D being non empty set, f1,f2 being FinSequence of D, n st 1
  <= n & n <= len f2 holds (f1^f2)/.(n + len f1) = f2/.n;

theorem :: SEQ_4:137
  v is increasing implies for n,m st n in dom v & m in dom v & n<=m
  holds v.n <= v.m;

theorem :: SEQ_4:138
  v is increasing implies for n,m st n in dom v & m in dom v & n<>
  m holds v.n<>v.m;

theorem :: SEQ_4:139
  v is increasing & v1 = v|Seg n implies v1 is increasing;

theorem :: SEQ_4:140
  for v holds ex v1 st rng v1 = rng v & len v1 = card rng v & v1 is
  increasing;

theorem :: SEQ_4:141
  for v1,v2 st len v1 = len v2 & rng v1 = rng v2 & v1 is increasing & v2
  is increasing holds v1 = v2;

definition
  let v;
  func Incr(v) ->increasing FinSequence of REAL means
:: SEQ_4:def 21

  rng it = rng v & len it = card rng v;
end;

registration
  let v be non empty FinSequence of REAL;
  cluster Incr v -> non empty;
end;

:: from SPRECT_1, 2011.04.24, A.T

registration
  cluster non empty bounded_above bounded_below for Subset of REAL;
end;

theorem :: SEQ_4:142
  for A,B being non empty bounded_below Subset of REAL holds lower_bound(A
  \/ B) = min(lower_bound A,lower_bound B);

theorem :: SEQ_4:143
  for A,B being non empty bounded_above Subset of REAL holds upper_bound(A
  \/ B) = max(upper_bound A,upper_bound B);

:: from TOPMETR3, 2011.04.24, A.T

theorem :: SEQ_4:144
  for R being non empty Subset of REAL,r0 being Real st for
  r being Real st r in R holds r <= r0 holds upper_bound R <= r0;