:: Introduction to Banach and Hilbert spaces - Part II
:: by Jan Popio{\l}ek
::
:: Received July 19, 1991
:: Copyright (c) 1991-2026 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, BHSP_1, PRE_TOPC, REAL_1, NAT_1, SUBSET_1, SUPINF_2,
SEQ_2, XXREAL_0, CARD_1, METRIC_1, FUNCT_1, ARYTM_3, ARYTM_1, RELAT_1,
COMPLEX1, NORMSP_1, ORDINAL2, SEQ_1, TARSKI, STRUCT_0, XBOOLE_0;
notations TARSKI, ORDINAL1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1,
REAL_1, NAT_1, SEQ_1, COMSEQ_2, SEQ_2, RELAT_1, VALUED_0, STRUCT_0,
PRE_TOPC, RLVECT_1, VFUNCT_1, BHSP_1, NORMSP_1, XXREAL_0;
constructors DOMAIN_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1, SEQ_2, BHSP_1,
VALUED_1, RELSET_1, VFUNCT_1, COMSEQ_2;
registrations ORDINAL1, RELSET_1, XREAL_0, STRUCT_0, VFUNCT_1, FUNCT_2, NAT_1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
theorems TARSKI, NAT_1, FUNCT_1, SEQ_2, ABSVALUE, SUBSET_1, RLVECT_1, BHSP_1,
NORMSP_1, FUNCT_2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XREAL_1, COMPLEX1,
XXREAL_0, VALUED_0, ORDINAL1;
schemes SEQ_1, FRAENKEL;
begin
reserve X for RealUnitarySpace;
reserve x, y, z, g, g1, g2 for Point of X;
reserve a, q, r for Real;
reserve seq, seq1, seq2, seq9 for sequence of X;
reserve k, n, m, m1, m2 for Nat;
deffunc 09(RealUnitarySpace) = 0. $1;
definition
let X, seq;
attr seq is convergent means
ex g st for r st r > 0 ex m st for n st n >= m holds dist(seq.n, g) < r;
end;
registration let X;
cluster constant -> convergent for sequence of X;
coherence
proof let seq be sequence of X;
assume seq is constant;
then consider x such that
A1: for n being Nat holds seq.n = x by VALUED_0:def 18;
take g = x;
let r such that
A2: r > 0;
take m = 0;
let n such that
n >= m;
dist(seq.n, g) = dist(x, g) by A1
.= 0 by BHSP_1:34;
hence thesis by A2;
end;
end;
theorem
seq is constant implies seq is convergent;
theorem Th2:
seq is convergent & (ex k st for n st k <= n holds seq9.n = seq.n
) implies seq9 is convergent
proof
assume that
A1: seq is convergent and
A2: ex k st for n st k <= n holds seq9.n = seq.n;
consider k such that
A3: for n st n >= k holds seq9.n = seq.n by A2;
consider g such that
A4: for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , g) < r
by A1;
take h = g;
let r;
assume r > 0;
then consider m1 such that
A5: for n st n >= m1 holds dist((seq.n) , h) < r by A4;
A6: now
assume
A7: m1 <= k;
take m = k;
let n;
assume
A8: n >= m;
then n >= m1 by A7,XXREAL_0:2;
then dist((seq.n) , g) < r by A5;
hence dist((seq9.n) , h) < r by A3,A8;
end;
now
assume
A9: k <= m1;
take m = m1;
let n;
assume
A10: n >= m;
then seq9.n = seq.n by A3,A9,XXREAL_0:2;
hence dist((seq9.n) , h) < r by A5,A10;
end;
hence thesis by A6;
end;
theorem Th3:
seq1 is convergent & seq2 is convergent implies seq1 + seq2 is convergent
proof
assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
consider g1 such that
A3: for r st r > 0 ex m st for n st n >= m holds dist((seq1.n) , g1) < r
by A1;
consider g2 such that
A4: for r st r > 0 ex m st for n st n >= m holds dist((seq2.n) , g2) < r
by A2;
take g = g1 + g2;
let r;
assume
A5: r > 0;
then consider m1 such that
A6: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A3,XREAL_1:215;
consider m2 such that
A7: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A4,A5,XREAL_1:215;
reconsider k = m1 + m2 as Nat;
take k;
let n be Nat such that
A8: n >= k;
k >= m2 by NAT_1:12;
then n >= m2 by A8,XXREAL_0:2;
then
A9: dist((seq2.n) , g2) < r/2 by A7;
dist((seq1 + seq2).n, g) = dist((seq1.n) + (seq2.n) , (g1 + g2)) by
NORMSP_1:def 2;
then
A10: dist((seq1 + seq2).n, g) <= dist((seq1.n) , g1) + dist((seq2.n) , g2)
by BHSP_1:40;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A8,XXREAL_0:2;
then dist((seq1.n) , g1) < r/2 by A6;
then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2 by A9,XREAL_1:8;
hence thesis by A10,XXREAL_0:2;
end;
theorem Th4:
seq1 is convergent & seq2 is convergent implies seq1 - seq2 is convergent
proof
assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
consider g1 such that
A3: for r st r > 0 ex m st for n st n >= m holds dist((seq1.n) , g1) < r
by A1;
consider g2 such that
A4: for r st r > 0 ex m st for n st n >= m holds dist((seq2.n) , g2) < r
by A2;
take g = g1 - g2;
let r;
assume
A5: r > 0;
then consider m1 such that
A6: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A3,XREAL_1:215;
consider m2 such that
A7: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A4,A5,XREAL_1:215;
take k = m1 + m2;
let n such that
A8: n >= k;
k >= m2 by NAT_1:12;
then n >= m2 by A8,XXREAL_0:2;
then
A9: dist((seq2.n) , g2) < r/2 by A7;
dist((seq1 - seq2).n, g) = dist((seq1.n) - (seq2.n) , (g1 - g2)) by
NORMSP_1:def 3;
then
A10: dist((seq1 - seq2).n, g) <= dist((seq1.n) , g1) + dist((seq2.n) , g2)
by BHSP_1:41;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A8,XXREAL_0:2;
then dist((seq1.n) , g1) < r/2 by A6;
then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2 by A9,XREAL_1:8;
hence thesis by A10,XXREAL_0:2;
end;
theorem Th5:
seq is convergent implies a * seq is convergent
proof
assume seq is convergent;
then consider g such that
A1: for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , g) < r;
take h = a * g;
A2: now
A3: 0/|.a.| = 0;
assume
A4: a <> 0;
then
A5: |.a.| > 0 by COMPLEX1:47;
let r;
assume r > 0;
then consider m1 such that
A6: for n st n >= m1 holds dist(seq.n, g) < r/|.a.| by A1,A5,A3,XREAL_1:74;
take k = m1;
let n;
assume n >= k;
then
A7: dist((seq.n) , g) < r/|.a.| by A6;
A8: |.a.| <> 0 by A4,COMPLEX1:47;
A9: |.a.| * (r/|.a.|) = |.a.| * (|.a.|" * r) by XCMPLX_0:def 9
.= |.a.| *|.a.|" * r
.= 1 * r by A8,XCMPLX_0:def 7
.= r;
dist(a * (seq.n) , a * g) = ||.(a * (seq.n)) - (a * g).|| by BHSP_1:def 5
.= ||.a * ((seq.n) - g).|| by RLVECT_1:34
.= |.a.| * ||.(seq.n) - g.|| by BHSP_1:27
.= |.a.| * dist((seq.n) , g) by BHSP_1:def 5;
then dist((a *(seq.n)) , h) < r by A5,A7,A9,XREAL_1:68;
hence dist((a * seq).n, h) < r by NORMSP_1:def 5;
end;
now
assume
A10: a = 0;
let r;
assume r > 0;
then consider m1 such that
A11: for n st n >= m1 holds dist((seq.n) , g) < r by A1;
take k = m1;
let n;
assume n >= k;
then
A12: dist((seq.n) , g) < r by A11;
dist(a * (seq.n) , a * g) = dist(0 * (seq.n) , 09(X)) by A10,RLVECT_1:10
.= dist(09(X) , 09(X)) by RLVECT_1:10
.= 0 by BHSP_1:34;
then dist(a * (seq.n) , h) < r by A12,BHSP_1:37;
hence dist((a * seq).n, h) < r by NORMSP_1:def 5;
end;
hence thesis by A2;
end;
theorem Th6:
seq is convergent implies - seq is convergent
proof
assume seq is convergent;
then (-1) * seq is convergent by Th5;
hence thesis by BHSP_1:55;
end;
theorem Th7:
seq is convergent implies seq + x is convergent
proof
assume seq is convergent;
then consider g such that
A1: for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , g) < r;
take g + x;
let r;
assume r > 0;
then consider m1 such that
A2: for n st n >= m1 holds dist((seq.n) , g) < r by A1;
take k = m1;
let n;
dist((seq.n) + x, g + x) <= dist((seq.n) , g) + dist(x, x) by BHSP_1:40;
then
A3: dist((seq.n) + x, g + x) <= dist((seq.n) , g) + 0 by BHSP_1:34;
assume n >= k;
then dist((seq.n) , g) < r by A2;
then dist((seq.n) + x, g + x) < r by A3,XXREAL_0:2;
hence thesis by BHSP_1:def 6;
end;
theorem Th8:
seq is convergent implies seq - x is convergent
proof
assume seq is convergent;
then seq + (-x) is convergent by Th7;
hence thesis by BHSP_1:56;
end;
theorem Th9:
seq is convergent iff ex g st for r st r > 0 ex m st for n st n
>= m holds ||.(seq.n) - g.|| < r
proof
thus seq is convergent implies ex g st for r st r > 0 ex m st for n st n >=
m holds ||.(seq.n) - g.|| < r
proof
assume seq is convergent;
then consider g such that
A1: for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , g) < r;
take g;
let r;
assume r > 0;
then consider m1 such that
A2: for n st n >= m1 holds dist((seq.n) , g) < r by A1;
take k = m1;
let n;
assume n >= k;
then dist((seq.n) , g) < r by A2;
hence thesis by BHSP_1:def 5;
end;
( ex g st for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.||
< r ) implies seq is convergent
proof
given g such that
A3: for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.|| < r;
take g;
let r;
assume r > 0;
then consider m1 such that
A4: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A3;
take k = m1;
let n;
assume n >= k;
then ||.(seq.n) - g.|| < r by A4;
hence thesis by BHSP_1:def 5;
end;
hence thesis;
end;
definition
let X, seq;
assume
A1: seq is convergent;
func lim seq -> Point of X means
:Def2:
for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , it) < r;
existence by A1;
uniqueness
proof
for x, y st ( for r st r > 0 ex m st for n st n >= m holds dist((seq.n
) , x) < r ) & ( for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , y)
< r ) holds x = y
proof
given x, y such that
A2: for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , x) < r and
A3: for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , y) < r and
A4: x <> y;
A5: dist(x, y) > 0 by A4,BHSP_1:38;
then
A6: dist(x, y)/4 > 0/4 by XREAL_1:74;
then consider m1 such that
A7: for n st n >= m1 holds dist((seq.n) , x) < dist(x, y)/4 by A2;
consider m2 such that
A8: for n st n >= m2 holds dist((seq.n) , y) < dist(x, y)/4 by A3,A6;
A9: now
assume m1 >= m2;
then
A10: dist((seq.m1) , y) < dist(x, y)/4 by A8;
dist(x, y) = dist(x - (seq.m1) , y - (seq.m1)) by BHSP_1:42;
then
A11: dist(x, y) <= dist((seq.m1) , x) + dist((seq.m1) , y) by BHSP_1:43;
dist((seq.m1) , x) < dist(x, y)/4 by A7;
then dist((seq.m1) , x) + dist((seq.m1) , y) < dist(x, y)/4 + dist(x,
y) /4 by A10,XREAL_1:8;
then dist(x, y) <= dist(x, y)/2 by A11,XXREAL_0:2;
hence contradiction by A5,XREAL_1:216;
end;
now
assume m1 <= m2;
then
A12: dist((seq.m2) , x) < dist(x, y)/4 by A7;
dist(x, y) = dist(x - (seq.m2) , y - (seq.m2)) by BHSP_1:42;
then
A13: dist(x, y) <= dist((seq.m2) , x) + dist((seq.m2) , y) by BHSP_1:43;
dist((seq.m2) , y) < dist(x, y)/4 by A8;
then dist((seq.m2) , x) + dist((seq.m2) , y) < dist(x, y)/4 + dist(x,
y)/4 by A12,XREAL_1:8;
then dist(x, y) <= dist(x, y)/2 by A13,XXREAL_0:2;
hence contradiction by A5,XREAL_1:216;
end;
hence contradiction by A9;
end;
hence thesis;
end;
end;
theorem Th10:
seq is constant & x in rng seq implies lim seq = x
proof
assume that
A1: seq is constant and
A2: x in rng seq;
consider y such that
A3: rng seq = {y} by A1,FUNCT_2:111;
consider z such that
A4: for n being Nat holds seq.n = z by A1,VALUED_0:def 18;
A5: x = y by A2,A3,TARSKI:def 1;
A6: now
let r such that
A7: r > 0;
reconsider m = 0 as Nat;
take m;
let n such that
n >= m;
n in NAT by ORDINAL1:def 12;
then n in dom seq by NORMSP_1:12;
then seq.n in rng seq by FUNCT_1:def 3;
then z in rng seq by A4;
then z = x by A3,A5,TARSKI:def 1;
then seq.n = x by A4;
hence dist((seq.n) , x) < r by A7,BHSP_1:34;
end;
seq is convergent by A1;
hence thesis by A6,Def2;
end;
theorem
seq is constant & (ex n st seq.n = x) implies lim seq = x
proof
assume that
A1: seq is constant and
A2: ex n st seq.n = x;
consider n such that
A3: seq.n = x by A2;
n in NAT by ORDINAL1:def 12;
then n in dom seq by NORMSP_1:12;
then x in rng seq by A3,FUNCT_1:def 3;
hence thesis by A1,Th10;
end;
theorem
seq is convergent & (ex k st for n st n >= k holds seq9.n = seq.n)
implies lim seq = lim seq9
proof
assume that
A1: seq is convergent and
A2: ex k st for n st n >= k holds seq9.n = seq.n;
consider k such that
A3: for n st n >= k holds seq9.n = seq.n by A2;
A4: now
let r;
assume r > 0;
then consider m1 such that
A5: for n st n >= m1 holds dist((seq.n) , (lim seq)) < r by A1,Def2;
A6: now
assume
A7: m1 <= k;
take m = k;
let n;
assume
A8: n >= m;
then n >= m1 by A7,XXREAL_0:2;
then dist((seq.n) , (lim seq)) < r by A5;
hence dist((seq9.n) , (lim seq)) < r by A3,A8;
end;
now
assume
A9: k <= m1;
take m = m1;
let n;
assume
A10: n >= m;
then seq9.n = seq.n by A3,A9,XXREAL_0:2;
hence dist((seq9.n) , (lim seq)) < r by A5,A10;
end;
hence ex m st for n st n >= m holds dist((seq9.n) , (lim seq)) < r by A6;
end;
seq9 is convergent by A1,A2,Th2;
hence thesis by A4,Def2;
end;
theorem Th13:
seq1 is convergent & seq2 is convergent implies lim (seq1 + seq2
) = (lim seq1) + (lim seq2)
proof
assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
set g2 = lim seq2;
set g1 = lim seq1;
set g = g1 + g2;
A3: now
let r;
assume r > 0;
then
A4: r/2 > 0 by XREAL_1:215;
then consider m1 such that
A5: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A1,Def2;
consider m2 such that
A6: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A2,A4,Def2;
take k = m1 + m2;
let n such that
A7: n >= k;
k >= m2 by NAT_1:12;
then n >= m2 by A7,XXREAL_0:2;
then
A8: dist((seq2.n) , g2) < r/2 by A6;
dist((seq1 + seq2).n, g) = dist((seq1.n) + (seq2.n) , g1 + g2) by
NORMSP_1:def 2;
then
A9: dist((seq1 + seq2).n, g) <= dist((seq1.n) , g1) + dist((seq2.n) , g2)
by BHSP_1:40;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A7,XXREAL_0:2;
then dist((seq1.n) , g1) < r/2 by A5;
then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2 by A8,XREAL_1:8;
hence dist((seq1 + seq2).n, g) < r by A9,XXREAL_0:2;
end;
seq1 + seq2 is convergent by A1,A2,Th3;
hence thesis by A3,Def2;
end;
theorem Th14:
seq1 is convergent & seq2 is convergent implies lim (seq1 - seq2
) = (lim seq1) - (lim seq2)
proof
assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
set g2 = lim seq2;
set g1 = lim seq1;
set g = g1 - g2;
A3: now
let r;
assume r > 0;
then
A4: r/2 > 0 by XREAL_1:215;
then consider m1 such that
A5: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A1,Def2;
consider m2 such that
A6: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A2,A4,Def2;
take k = m1 + m2;
let n such that
A7: n >= k;
k >= m2 by NAT_1:12;
then n >= m2 by A7,XXREAL_0:2;
then
A8: dist((seq2.n) , g2) < r/2 by A6;
dist((seq1 - seq2).n, g) = dist((seq1.n) - (seq2.n) , g1 - g2) by
NORMSP_1:def 3;
then
A9: dist((seq1 - seq2).n, g) <= dist((seq1.n) , g1) + dist((seq2.n) , g2)
by BHSP_1:41;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A7,XXREAL_0:2;
then dist((seq1.n) , g1) < r/2 by A5;
then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2 by A8,XREAL_1:8;
hence dist((seq1 - seq2).n, g) < r by A9,XXREAL_0:2;
end;
seq1 - seq2 is convergent by A1,A2,Th4;
hence thesis by A3,Def2;
end;
theorem Th15:
seq is convergent implies lim (a * seq) = a * (lim seq)
proof
set g = lim seq;
set h = a * g;
assume
A1: seq is convergent;
A2: now
assume
A3: a = 0;
let r;
assume r > 0;
then consider m1 such that
A4: for n st n >= m1 holds dist((seq.n) , g) < r by A1,Def2;
take k = m1;
let n;
assume n >= k;
then
A5: dist((seq.n) , g) < r by A4;
dist(a * (seq.n) , a * g) = dist(0 * (seq.n) , 09(X)) by A3,RLVECT_1:10
.= dist(09(X) , 09(X)) by RLVECT_1:10
.= 0 by BHSP_1:34;
then dist(a * (seq.n) , h) < r by A5,BHSP_1:37;
hence dist((a * seq).n, h) < r by NORMSP_1:def 5;
end;
A6: now
A7: 0/|.a.| =0;
assume
A8: a <> 0;
then
A9: |.a.| > 0 by COMPLEX1:47;
let r;
assume r > 0;
then r/|.a.| > 0 by A9,A7,XREAL_1:74;
then consider m1 such that
A10: for n st n >= m1 holds dist((seq.n) , g) < r/|.a.| by A1,Def2;
take k = m1;
let n;
assume n >= k;
then
A11: dist((seq.n) , g) < r/|.a.| by A10;
A12: |.a.| <> 0 by A8,COMPLEX1:47;
A13: |.a.| * (r/|.a.|) = |.a.| * (|.a.|" * r) by XCMPLX_0:def 9
.= |.a.| *|.a.|" * r
.= 1 * r by A12,XCMPLX_0:def 7
.= r;
dist(a * (seq.n) , a * g) = ||.(a * (seq.n)) - (a * g).|| by BHSP_1:def 5
.= ||.a * ((seq.n) - g).|| by RLVECT_1:34
.= |.a.| * ||.(seq.n) - g.|| by BHSP_1:27
.= |.a.| * dist((seq.n) , g) by BHSP_1:def 5;
then dist(a * (seq.n) , h) < r by A9,A11,A13,XREAL_1:68;
hence dist((a * seq).n, h) < r by NORMSP_1:def 5;
end;
a * seq is convergent by A1,Th5;
hence thesis by A2,A6,Def2;
end;
theorem Th16:
seq is convergent implies lim (- seq) = - (lim seq)
proof
assume seq is convergent;
then lim ((-1) * seq) = (-1) * (lim seq) by Th15;
then lim (- seq) = (-1) * (lim seq) by BHSP_1:55;
hence thesis by RLVECT_1:16;
end;
theorem Th17:
seq is convergent implies lim (seq + x) = (lim seq) + x
proof
set g = lim seq;
assume
A1: seq is convergent;
A2: now
let r;
assume r > 0;
then consider m1 such that
A3: for n st n >= m1 holds dist((seq.n) , g) < r by A1,Def2;
take k = m1;
let n;
assume n >= k;
then
A4: dist((seq.n) , g) < r by A3;
dist((seq.n) , g) = dist((seq.n) - (-x) , g - (-x)) by BHSP_1:42
.= dist((seq.n) + (-(-x)) , g - (-x)) by RLVECT_1:def 11
.= dist((seq.n) + x, g - (-x)) by RLVECT_1:17
.= dist((seq.n) + x, g + (-(-x))) by RLVECT_1:def 11
.= dist((seq.n) + x, g + x) by RLVECT_1:17;
hence dist((seq + x).n, (g + x)) < r by A4,BHSP_1:def 6;
end;
seq + x is convergent by A1,Th7;
hence thesis by A2,Def2;
end;
theorem
seq is convergent implies lim (seq - x) = (lim seq) - x
proof
assume seq is convergent;
then lim (seq + (-x)) = (lim seq) + (-x) by Th17;
then lim (seq - x) = (lim seq) + (-x) by BHSP_1:56;
hence thesis by RLVECT_1:def 11;
end;
theorem Th19:
seq is convergent implies ( lim seq = g iff for r st r > 0 ex m
st for n st n >= m holds ||.(seq.n) - g.|| < r )
proof
assume
A1: seq is convergent;
thus lim seq = g implies for r st r > 0 ex m st for n st n >= m holds ||.(
seq.n) - g.|| < r
proof
assume
A2: lim seq = g;
let r;
assume r > 0;
then consider m1 such that
A3: for n st n >= m1 holds dist((seq.n) , g) < r by A1,A2,Def2;
take k = m1;
let n;
assume n >= k;
then dist((seq.n) , g) < r by A3;
hence thesis by BHSP_1:def 5;
end;
( for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.|| < r )
implies lim seq = g
proof
assume
A4: for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.|| < r;
now
let r;
assume r > 0;
then consider m1 such that
A5: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A4;
take k = m1;
let n;
assume n >= k;
then ||.(seq.n) - g.|| < r by A5;
hence dist((seq.n) , g) < r by BHSP_1:def 5;
end;
hence thesis by A1,Def2;
end;
hence thesis;
end;
definition
let X, seq;
func ||.seq.|| -> Real_Sequence means
:Def3:
for n holds it.n =||.(seq.n).||;
existence
proof
deffunc F(Nat) = ||.(seq.$1).||;
consider s being Real_Sequence such that
A1: for n being Nat holds s.n = F(n) from SEQ_1:sch 1;
take s;
thus thesis by A1;
end;
uniqueness
proof
let s,t be Real_Sequence;
assume that
A2: for n holds s.n = ||.(seq.n).|| and
A3: for n holds t.n = ||.(seq.n).||;
now
let n be Element of NAT;
s.n = ||.(seq.n).|| by A2;
hence s.n = t.n by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th20:
seq is convergent implies ||.seq.|| is convergent
proof
assume seq is convergent;
then consider g such that
A1: for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.|| < r by Th9;
now
let r be Real;
assume
A2: r > 0;
consider m1 such that
A3: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A1,A2;
reconsider k = m1 as Nat;
take k;
now
let n be Nat;
assume n >= k;
then
A4: ||.(seq.n) - g.|| < r by A3;
|.||.(seq.n).|| - ||.g.||.| <= ||.(seq.n) - g.|| by BHSP_1:33;
then |.||.(seq.n).|| - ||.g.||.| < r by A4,XXREAL_0:2;
hence |.||.seq.||.n - ||.g.||.| < r by Def3;
end;
hence for n being Nat st k <= n holds |.||.seq.||.n - ||.g.||.| < r;
end;
hence thesis by SEQ_2:def 6;
end;
theorem Th21:
seq is convergent & lim seq = g implies ||.seq.|| is convergent
& lim ||.seq.|| = ||.g.||
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
A3: now
let r be Real;
assume
A4: r > 0;
consider m1 such that
A5: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A1,A2,A4,Th19;
reconsider k = m1 as Nat;
take k;
now
let n be Nat;
assume n >= k;
then
A6: ||.(seq.n) - g.|| < r by A5;
|.||.(seq.n).|| - ||.g.||.| <= ||.(seq.n) - g.|| by BHSP_1:33;
then |.||.(seq.n).|| - ||.g.||.| < r by A6,XXREAL_0:2;
hence |.||.seq.||.n - ||.g.||.| < r by Def3;
end;
hence for n being Nat st k <= n holds |.||.seq.||.n - ||.g.||.| < r;
end;
||.seq.|| is convergent by A1,Th20;
hence thesis by A3,SEQ_2:def 7;
end;
theorem Th22:
seq is convergent & lim seq = g implies ||.seq - g.|| is
convergent & lim ||.seq - g.|| = 0
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
A3: now
let r be Real;
assume
A4: r > 0;
consider m1 such that
A5: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A1,A2,A4,Th19;
reconsider k = m1 as Nat;
take k;
let n be Nat;
assume n >= k;
then ||.(seq.n) - g.|| < r by A5;
then
A6: ||.((seq.n) - g ) - 09(X).|| < r by RLVECT_1:13;
|.||.(seq.n) - g.|| - ||.09(X).||.| <= ||.((seq.n) - g ) - 09( X )
.|| by BHSP_1:33;
then |.||.(seq.n) - g.|| - ||.09(X).||.| < r by A6,XXREAL_0:2;
then |.(||.(seq.n) - g.|| - 0).| < r by BHSP_1:26;
then |.(||.(seq - g).n.|| - 0).| < r by NORMSP_1:def 4;
hence |.(||.seq - g.||.n - 0).| < r by Def3;
end;
||.seq - g.|| is convergent by A1,Th8,Th20;
hence thesis by A3,SEQ_2:def 7;
end;
definition
let X;
let seq;
let x;
func dist(seq, x) -> Real_Sequence means
:Def4:
for n holds it.n =dist((seq. n) , x);
existence
proof
deffunc F(Nat) = dist((seq.$1) , x);
consider s being Real_Sequence such that
A1: for n being Nat holds s.n = F(n) from SEQ_1:sch 1;
take s;
thus thesis by A1;
end;
uniqueness
proof
let s,t be Real_Sequence;
assume that
A2: for n holds s.n = dist((seq.n) , x) and
A3: for n holds t.n = dist((seq.n) , x);
now
let n be Element of NAT;
s.n = dist((seq.n) , x) by A2;
hence s.n = t.n by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th23:
seq is convergent & lim seq = g implies dist(seq, g) is convergent
proof
assume
A1: seq is convergent & lim seq = g;
now
let r be Real;
assume
A2: r > 0;
consider m1 such that
A3: for n st n >= m1 holds dist((seq.n) , g) < r by A1,A2,Def2;
reconsider k = m1 as Nat;
take k;
now
let n be Nat;
dist((seq.n) , g) >= 0 by BHSP_1:37;
then
A4: |.(dist((seq.n) , g) - 0).| = dist((seq.n) , g) by ABSVALUE:def 1;
assume n >= k;
then dist((seq.n) , g) < r by A3;
hence |.(dist(seq, g).n - 0).| < r by A4,Def4;
end;
hence for n being Nat st k <= n holds |.(dist(seq, g).n - 0).| < r;
end;
hence thesis by SEQ_2:def 6;
end;
theorem Th24:
seq is convergent & lim seq = g implies dist(seq, g) is
convergent & lim dist(seq, g) = 0
proof
assume
A1: seq is convergent & lim seq = g;
A2: now
let r be Real;
assume
A3: r > 0;
consider m1 such that
A4: for n st n >= m1 holds dist((seq.n) , g) < r by A1,A3,Def2;
reconsider k = m1 as Nat;
take k;
let n be Nat;
dist((seq.n) , g) >= 0 by BHSP_1:37;
then
A5: |.(dist((seq.n) , g) - 0).| = dist((seq.n) , g) by ABSVALUE:def 1;
assume n >= k;
then dist((seq.n) , g) < r by A4;
hence |.(dist(seq, g).n - 0).| < r by A5,Def4;
end;
dist(seq, g) is convergent by A1,Th23;
hence thesis by A2,SEQ_2:def 7;
end;
theorem
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies ||.seq1 + seq2.|| is convergent & lim ||.seq1 + seq2.|| = ||.g1 + g2
.||
proof
assume
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2;
then seq1 + seq2 is convergent & lim (seq1 + seq2) = g1 + g2 by Th3,Th13;
hence thesis by Th21;
end;
theorem
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies ||.(seq1 + seq2) - (g1 + g2).|| is convergent & lim ||.(seq1 + seq2)
- (g1 + g2).|| = 0
proof
assume
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2;
then seq1 + seq2 is convergent & lim (seq1 + seq2) = g1 + g2 by Th3,Th13;
hence thesis by Th22;
end;
theorem
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies ||.seq1 - seq2.|| is convergent & lim ||.seq1 - seq2.|| = ||.g1 - g2
.||
proof
assume
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2;
then seq1 - seq2 is convergent & lim (seq1 - seq2) = g1 - g2 by Th4,Th14;
hence thesis by Th21;
end;
theorem
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies ||.(seq1 - seq2) - (g1 - g2).|| is convergent & lim ||.(seq1 - seq2)
- (g1 - g2).|| = 0
proof
assume
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2;
then seq1 - seq2 is convergent & lim (seq1 - seq2) = g1 - g2 by Th4,Th14;
hence thesis by Th22;
end;
theorem
seq is convergent & lim seq = g implies ||.a * seq.|| is convergent &
lim ||.a * seq.|| = ||.a * g.||
proof
assume seq is convergent & lim seq = g;
then a * seq is convergent & lim (a * seq) = a * g by Th5,Th15;
hence thesis by Th21;
end;
theorem
seq is convergent & lim seq = g implies ||.(a * seq) - (a * g).|| is
convergent & lim ||.(a * seq) - (a * g).|| = 0
proof
assume seq is convergent & lim seq = g;
then a * seq is convergent & lim (a * seq) = a * g by Th5,Th15;
hence thesis by Th22;
end;
theorem
seq is convergent & lim seq = g implies ||.- seq.|| is convergent &
lim ||.- seq.|| = ||.- g.||
proof
assume seq is convergent & lim seq = g;
then - seq is convergent & lim (- seq) = - g by Th6,Th16;
hence thesis by Th21;
end;
theorem
seq is convergent & lim seq = g implies ||.(- seq) - (- g).|| is
convergent & lim ||.(- seq) - (- g).|| = 0
proof
assume seq is convergent & lim seq = g;
then - seq is convergent & lim (- seq) = - g by Th6,Th16;
hence thesis by Th22;
end;
Lm1: seq is convergent & lim seq = g implies ||.seq + x.|| is convergent & lim
||.seq + x.|| = ||.g + x.||
proof
assume seq is convergent & lim seq = g;
then seq + x is convergent & lim (seq + x) = g + x by Th7,Th17;
hence thesis by Th21;
end;
theorem Th33:
seq is convergent & lim seq = g implies ||.(seq + x) - (g + x)
.|| is convergent & lim ||.(seq + x) - (g + x).|| = 0
proof
assume seq is convergent & lim seq = g;
then seq + x is convergent & lim (seq + x) = g + x by Th7,Th17;
hence thesis by Th22;
end;
theorem
seq is convergent & lim seq = g implies ||.seq - x.|| is convergent &
lim ||.seq - x.|| = ||.g - x.||
proof
assume
A1: seq is convergent & lim seq = g;
then lim ||.seq + (-x).|| = ||.g + (-x).|| by Lm1;
then
A2: lim ||.seq - x.|| = ||.g + (-x).|| by BHSP_1:56;
||.seq + (-x).|| is convergent by A1,Lm1;
hence thesis by A2,BHSP_1:56,RLVECT_1:def 11;
end;
theorem
seq is convergent & lim seq = g implies ||.(seq - x) - (g - x).|| is
convergent & lim ||.(seq - x) - (g - x).|| = 0
proof
assume
A1: seq is convergent & lim seq = g;
then lim ||.(seq + (-x)) - (g + (-x)).|| = 0 by Th33;
then
A2: lim ||.(seq - x) - (g + (-x)).|| = 0 by BHSP_1:56;
||.(seq + (-x)) - (g + (-x)).|| is convergent by A1,Th33;
then ||.(seq - x) - (g + (-x)).|| is convergent by BHSP_1:56;
hence thesis by A2,RLVECT_1:def 11;
end;
theorem
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies dist((seq1 + seq2) , (g1 + g2)) is convergent & lim dist((seq1 +
seq2) , (g1 + g2)) = 0
proof
assume
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2;
then seq1 + seq2 is convergent & lim (seq1 + seq2) = g1 + g2 by Th3,Th13;
hence thesis by Th24;
end;
theorem
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies dist((seq1 - seq2) , (g1 - g2)) is convergent & lim dist((seq1 -
seq2) , (g1 - g2)) = 0
proof
assume
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2;
then seq1 - seq2 is convergent & lim (seq1 - seq2) = g1 - g2 by Th4,Th14;
hence thesis by Th24;
end;
theorem
seq is convergent & lim seq = g implies dist((a * seq) , (a * g)) is
convergent & lim dist((a * seq) , (a * g)) = 0
proof
assume seq is convergent & lim seq = g;
then a * seq is convergent & lim (a * seq) = a * g by Th5,Th15;
hence thesis by Th24;
end;
theorem
seq is convergent & lim seq = g implies dist((seq + x) , (g + x)) is
convergent & lim dist((seq + x) , (g + x)) = 0
proof
assume seq is convergent & lim seq = g;
then seq + x is convergent & lim (seq + x) = g + x by Th7,Th17;
hence thesis by Th24;
end;
definition
let X, x, r;
func Ball(x,r) -> Subset of X equals
{y where y is Point of X : ||.x - y.||
< r};
coherence
proof
defpred P[Point of X] means ||.x - $1.|| < r;
{y where y is Point of X : P[y]} c= the carrier of X from FRAENKEL:sch
10;
hence thesis;
end;
func cl_Ball(x,r) -> Subset of X equals
{y where y is Point of X : ||.x - y
.|| <= r};
coherence
proof
defpred P[Point of X] means ||.x - $1.|| <= r;
{y where y is Point of X : P[y]} c= the carrier of X from FRAENKEL:sch
10;
hence thesis;
end;
func Sphere(x,r) -> Subset of X equals
{y where y is Point of X : ||.x - y
.|| = r};
coherence
proof
defpred P[Point of X] means ||.x - $1.|| = r;
{y where y is Point of X : P[y]} c= the carrier of X from FRAENKEL:sch
10;
hence thesis;
end;
end;
theorem Th40:
z in Ball(x,r) iff ||.x - z.|| < r
proof
thus z in Ball(x,r) implies ||.x - z.|| < r
proof
assume z in Ball(x,r);
then ex y be Point of X st z = y & ||.x - y.|| < r;
hence thesis;
end;
thus thesis;
end;
theorem Th41:
z in Ball(x,r) iff dist(x,z) < r
proof
thus z in Ball(x,r) implies dist(x,z) < r
proof
assume z in Ball(x,r);
then ||.x - z.|| < r by Th40;
hence thesis by BHSP_1:def 5;
end;
assume dist(x,z) < r;
then ||.x - z.|| < r by BHSP_1:def 5;
hence thesis;
end;
theorem
r > 0 implies x in Ball(x,r)
proof
A1: dist(x,x) = 0 by BHSP_1:34;
assume r > 0;
hence thesis by A1,Th41;
end;
theorem
y in Ball(x,r) & z in Ball(x,r) implies dist(y,z) < 2 * r
proof
assume that
A1: y in Ball(x,r) and
A2: z in Ball(x,r);
dist(x,z) < r by A2,Th41;
then
A3: r + dist(x,z) < r + r by XREAL_1:6;
A4: dist(y,z) <= dist(y,x) + dist(x,z) by BHSP_1:35;
dist(x,y) < r by A1,Th41;
then dist(x,y) + dist(x,z) < r + dist(x,z) by XREAL_1:6;
then dist(x,y) + dist(x,z) < 2 * r by A3,XXREAL_0:2;
hence thesis by A4,XXREAL_0:2;
end;
theorem
y in Ball(x,r) implies y - z in Ball(x - z,r)
proof
assume y in Ball(x,r);
then
A1: dist(x,y) < r by Th41;
dist(x - z,y - z) = dist(x,y) by BHSP_1:42;
hence thesis by A1,Th41;
end;
theorem
y in Ball(x,r) implies (y - x) in Ball (0.(X),r)
proof
assume y in Ball(x,r);
then ||.x - y.|| < r by Th40;
then ||.(-y) + x.|| < r by RLVECT_1:def 11;
then ||.-(y - x).|| < r by RLVECT_1:33;
then ||.09(X) - (y - x).|| < r by RLVECT_1:14;
hence thesis;
end;
theorem
y in Ball(x,r) & r <= q implies y in Ball(x,q)
proof
assume that
A1: y in Ball(x,r) and
A2: r <= q;
||.x - y.|| < r by A1,Th40;
then ||.x - y.|| < q by A2,XXREAL_0:2;
hence thesis;
end;
theorem Th47:
z in cl_Ball(x,r) iff ||.x - z.|| <= r
proof
thus z in cl_Ball(x,r) implies ||.x - z.|| <= r
proof
assume z in cl_Ball(x,r);
then ex y be Point of X st z = y & ||.x - y.|| <= r;
hence thesis;
end;
assume ||.x - z.|| <= r;
hence thesis;
end;
theorem Th48:
z in cl_Ball(x,r) iff dist(x,z) <= r
proof
thus z in cl_Ball(x,r) implies dist(x,z) <= r
proof
assume z in cl_Ball(x,r);
then ||.x - z.|| <= r by Th47;
hence thesis by BHSP_1:def 5;
end;
assume dist(x,z) <= r;
then ||.x - z.|| <= r by BHSP_1:def 5;
hence thesis;
end;
theorem
r >= 0 implies x in cl_Ball(x,r)
proof
assume r >= 0;
then dist(x,x) <= r by BHSP_1:34;
hence thesis by Th48;
end;
theorem Th50:
y in Ball(x,r) implies y in cl_Ball(x,r)
proof
assume y in Ball(x,r);
then ||.x - y.|| <= r by Th40;
hence thesis;
end;
theorem Th51:
z in Sphere(x,r) iff ||.x - z.|| = r
proof
thus z in Sphere(x,r) implies ||.x - z.|| = r
proof
assume z in Sphere(x,r);
then ex y be Point of X st z = y & ||.x - y.|| = r;
hence thesis;
end;
assume ||.x - z.|| = r;
hence thesis;
end;
theorem
z in Sphere(x,r) iff dist(x,z) = r
proof
thus z in Sphere(x,r) implies dist(x,z) = r
proof
assume z in Sphere(x,r);
then ||.x - z.|| = r by Th51;
hence thesis by BHSP_1:def 5;
end;
assume dist(x,z) = r;
then ||.x - z.|| = r by BHSP_1:def 5;
hence thesis;
end;
theorem
y in Sphere(x,r) implies y in cl_Ball(x,r)
proof
assume y in Sphere(x,r);
then ||.x - y.|| = r by Th51;
hence thesis;
end;
theorem Th54:
Ball(x,r) c= cl_Ball(x,r)
proof
for y holds y in Ball(x,r) implies y in cl_Ball(x,r) by Th50;
hence thesis by SUBSET_1:2;
end;
theorem Th55:
Sphere(x,r) c= cl_Ball(x,r)
proof
now
let y;
assume y in Sphere(x,r);
then ||.x - y.|| = r by Th51;
hence y in cl_Ball(x,r);
end;
hence thesis by SUBSET_1:2;
end;
theorem
Ball(x,r) \/ Sphere(x,r) = cl_Ball(x,r)
proof
now
let y;
assume y in cl_Ball(x,r);
then
A1: ||.x - y.|| <= r by Th47;
now
per cases by A1,XXREAL_0:1;
case
||.x - y.|| < r;
hence y in Ball(x,r);
end;
case
||.x - y.|| = r;
hence y in Sphere(x,r);
end;
end;
hence y in Ball(x,r) \/ Sphere(x,r) by XBOOLE_0:def 3;
end;
then
A2: cl_Ball(x,r) c= Ball(x,r) \/ Sphere(x,r) by SUBSET_1:2;
Ball(x,r) c= cl_Ball(x,r) & Sphere(x,r) c= cl_Ball(x,r) by Th54,Th55;
then Ball(x,r) \/ Sphere(x,r) c= cl_Ball(x,r) by XBOOLE_1:8;
hence thesis by A2,XBOOLE_0:def 10;
end;