The abstract of the Mizar article:

Introduction to Banach and Hilbert Spaces --- Part III

by

Jan Popiolek

Received July 19, 1991

MML identifier: BHSP_3

[ Mizar article, MML identifier index ]

environ

 vocabulary BHSP_1, PRE_TOPC, NORMSP_1, ORDINAL2, SEQM_3, SEQ_1, RLVECT_1,
      METRIC_1, FUNCT_1, ARYTM_1, ARYTM_3, ABSVALUE, RELAT_1, SEQ_2, LATTICES,
      BHSP_3, ARYTM;
 notation TARSKI, ORDINAL1, NUMBERS, XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_1,
      FUNCT_2, SEQ_1, SEQM_3, ABSVALUE, STRUCT_0, PRE_TOPC, RLVECT_1, NORMSP_1,
      BHSP_1, BHSP_2;
 constructors REAL_1, NAT_1, SEQ_1, ABSVALUE, BHSP_2, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, SEQM_3, STRUCT_0, XREAL_0, RELSET_1, ARYTM_3, MEMBERED,
      ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

 reserve X for RealUnitarySpace,
         x, g, g1, h for Point of X,
         a, p, r, M, M1, M2 for Real,
         seq, seq1, seq2, seq3 for sequence of X,
         Nseq,Nseq1,Nseq2 for increasing Seq_of_Nat,
         Rseq for Real_Sequence,
         k, l, l1, l2, l3, n, m, m1, m2 for Nat;

definition
          let X;
          let seq;
          attr seq is Cauchy means
:: BHSP_3:def 1
    for r st r > 0 ex k st for n, m st ( n >= k & m >= k )
          holds dist((seq.n), (seq.m)) < r;
  synonym seq is_Cauchy_sequence;
end;

theorem :: BHSP_3:1
    seq is constant implies seq is_Cauchy_sequence;

theorem :: BHSP_3:2
    seq is_Cauchy_sequence iff for r st r > 0 ex k st for n, m st
    ( n >= k & m >= k ) holds ||.(seq.n) - (seq.m).|| < r;

theorem :: BHSP_3:3
    seq1 is_Cauchy_sequence & seq2 is_Cauchy_sequence implies
    seq1 + seq2 is_Cauchy_sequence;

theorem :: BHSP_3:4
    seq1 is_Cauchy_sequence & seq2 is_Cauchy_sequence implies
    seq1 - seq2 is_Cauchy_sequence;

theorem :: BHSP_3:5
  seq is_Cauchy_sequence implies a * seq is_Cauchy_sequence;

theorem :: BHSP_3:6
    seq is_Cauchy_sequence implies - seq is_Cauchy_sequence;

theorem :: BHSP_3:7
  seq is_Cauchy_sequence implies seq + x is_Cauchy_sequence;

theorem :: BHSP_3:8
    seq is_Cauchy_sequence implies seq - x is_Cauchy_sequence;

theorem :: BHSP_3:9
    seq is convergent implies seq is_Cauchy_sequence;

definition
          let X;
          let seq1, seq2;
          pred seq1 is_compared_to seq2 means
:: BHSP_3:def 2
    for r st r > 0 ex m st for n st n >= m holds
          dist(seq1.n, seq2.n) < r;
end;

theorem :: BHSP_3:10
  seq is_compared_to seq;

theorem :: BHSP_3:11
  seq1 is_compared_to seq2 implies seq2 is_compared_to seq1;

definition let X; let seq1, seq2;
  redefine pred seq1 is_compared_to seq2;
  reflexivity;
  symmetry;
end;

theorem :: BHSP_3:12
    seq1 is_compared_to seq2 & seq2 is_compared_to seq3
    implies seq1 is_compared_to seq3;

theorem :: BHSP_3:13
    seq1 is_compared_to seq2 iff for r st r > 0 ex m st
    for n st n >= m holds ||.(seq1.n) - (seq2.n).|| < r;

theorem :: BHSP_3:14
    ( ex k st for n st n >= k holds seq1.n = seq2.n )
    implies seq1 is_compared_to seq2;

theorem :: BHSP_3:15
    seq1 is_Cauchy_sequence & seq1 is_compared_to seq2
     implies seq2 is_Cauchy_sequence;

theorem :: BHSP_3:16
    seq1 is convergent & seq1 is_compared_to seq2
    implies seq2 is convergent;

theorem :: BHSP_3:17
    seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2
    implies seq2 is convergent & lim seq2 = g;

definition
          let X;
          let seq;
          attr seq is bounded means
:: BHSP_3:def 3
   ex M st M > 0 & for n holds ||.seq.n.|| <= M;
end;

theorem :: BHSP_3:18
  seq1 is bounded & seq2 is bounded implies seq1 + seq2 is bounded;

theorem :: BHSP_3:19
  seq is bounded implies -seq is bounded;

theorem :: BHSP_3:20
    seq1 is bounded & seq2 is bounded implies seq1 - seq2 is bounded;

theorem :: BHSP_3:21
    seq is bounded implies a * seq is bounded;

theorem :: BHSP_3:22
    seq is constant implies seq is bounded;

theorem :: BHSP_3:23
  for m ex M st ( M > 0 & for n st n <= m holds ||.seq.n.|| < M );

theorem :: BHSP_3:24
  seq is convergent implies seq is bounded;

theorem :: BHSP_3:25
    seq1 is bounded & seq1 is_compared_to seq2 implies seq2 is bounded;

definition let X, Nseq, seq;
  redefine func seq * Nseq -> sequence of X;
end;

definition let X be non empty 1-sorted,
               s1, s be sequence of X;
  pred s1 is_subsequence_of s means
:: BHSP_3:def 4
   ex N being increasing Seq_of_Nat st s1 = s * N;
end;

theorem :: BHSP_3:26
  for X being RealUnitarySpace,
      s being sequence of X,
      N being increasing Seq_of_Nat
  for n being Nat holds (s * N).n=s.(N.n);

theorem :: BHSP_3:27
    seq is_subsequence_of seq;

theorem :: BHSP_3:28
    seq1 is_subsequence_of seq2 & seq2 is_subsequence_of seq3
    implies seq1 is_subsequence_of seq3;

theorem :: BHSP_3:29
  seq is constant & seq1 is_subsequence_of seq implies seq1 is constant;

theorem :: BHSP_3:30
    seq is constant & seq1 is_subsequence_of seq implies seq = seq1;

theorem :: BHSP_3:31
  seq is bounded & seq1 is_subsequence_of seq implies seq1 is bounded;

theorem :: BHSP_3:32
  seq is convergent & seq1 is_subsequence_of seq implies seq1 is convergent;

theorem :: BHSP_3:33
  seq1 is_subsequence_of seq & seq is convergent implies lim seq1=lim seq;

theorem :: BHSP_3:34
  seq is_Cauchy_sequence & seq1 is_subsequence_of seq
    implies seq1 is_Cauchy_sequence;

definition
          let X;
          let seq;
          let k;
          func seq ^\k -> sequence of X means
:: BHSP_3:def 5
  for n holds it.n=seq.(n + k);
end;

theorem :: BHSP_3:35
    seq ^\0 = seq;

theorem :: BHSP_3:36
    (seq ^\k)^\m = (seq ^\m)^\k;

theorem :: BHSP_3:37
    (seq ^\k)^\m=seq ^\(k + m);

theorem :: BHSP_3:38
  (seq1 + seq2) ^\k = (seq1 ^\k) + (seq2 ^\k);

theorem :: BHSP_3:39
  (-seq) ^\k = -(seq ^\k);

theorem :: BHSP_3:40
    (seq1 - seq2) ^\k = (seq1 ^\k) - (seq2 ^\k);

theorem :: BHSP_3:41
    (a * seq) ^\k = a * (seq ^\k);

theorem :: BHSP_3:42
    (seq * Nseq) ^\k = seq * (Nseq ^\k);

theorem :: BHSP_3:43
  seq ^\k is_subsequence_of seq;

theorem :: BHSP_3:44
    seq is convergent implies ((seq ^\k) is convergent &
     lim (seq ^\k)=lim seq);

canceled;

theorem :: BHSP_3:46
    seq is convergent & (ex k st seq = seq1 ^\k) implies seq1 is convergent;

theorem :: BHSP_3:47
    seq is_Cauchy_sequence & (ex k st seq = seq1 ^\k)
    implies seq1 is_Cauchy_sequence;

theorem :: BHSP_3:48
    seq is_Cauchy_sequence implies (seq ^\k) is_Cauchy_sequence;

theorem :: BHSP_3:49
    seq1 is_compared_to seq2 implies (seq1 ^\k) is_compared_to (seq2 ^\k);

theorem :: BHSP_3:50
    seq is bounded implies (seq ^\k) is bounded;

theorem :: BHSP_3:51
    seq is constant implies (seq ^\k) is constant;

definition
          let X;
          attr X is complete means
:: BHSP_3:def 6
    for seq holds
          seq is_Cauchy_sequence implies seq is convergent;
  synonym X is_complete_space;
end;

canceled;

theorem :: BHSP_3:53
    X is_complete_space & seq is_Cauchy_sequence implies seq is bounded;

definition
          let X;
          attr X is Hilbert means
:: BHSP_3:def 7
            X is RealUnitarySpace & X is_complete_space;
  synonym X is_Hilbert_space;
end;