:: Introduction to Banach and Hilbert spaces - Part II
:: by Jan Popio{\l}ek
::
:: Copyright (c) 1991-2021 Association of Mizar Users

deffunc H1( RealUnitarySpace) -> Element of the carrier of $1 = 0.$1;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
attr seq is convergent means :: BHSP_2:def 1
ex g being Point of X st
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),g) < r;
end;

:: deftheorem defines convergent BHSP_2:def 1 :
for X being RealUnitarySpace
for seq being sequence of X holds
( seq is convergent iff ex g being Point of X st
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),g) < r );

registration
let X be RealUnitarySpace;
cluster V12() constant V32( NAT , the carrier of X) -> convergent for Element of K32(K33(NAT, the carrier of X));
coherence
for b1 being sequence of X st b1 is constant holds
b1 is convergent
proof end;
end;

theorem :: BHSP_2:1
for X being RealUnitarySpace
for seq being sequence of X st seq is constant holds
seq is convergent ;

theorem Th2: :: BHSP_2:2
for X being RealUnitarySpace
for seq, seq9 being sequence of X st seq is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq9 . n = seq . n holds
seq9 is convergent
proof end;

theorem Th3: :: BHSP_2:3
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
seq1 + seq2 is convergent
proof end;

theorem Th4: :: BHSP_2:4
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
seq1 - seq2 is convergent
proof end;

theorem Th5: :: BHSP_2:5
for X being RealUnitarySpace
for a being Real
for seq being sequence of X st seq is convergent holds
a * seq is convergent
proof end;

theorem Th6: :: BHSP_2:6
for X being RealUnitarySpace
for seq being sequence of X st seq is convergent holds
- seq is convergent
proof end;

theorem Th7: :: BHSP_2:7
for X being RealUnitarySpace
for x being Point of X
for seq being sequence of X st seq is convergent holds
seq + x is convergent
proof end;

theorem Th8: :: BHSP_2:8
for X being RealUnitarySpace
for x being Point of X
for seq being sequence of X st seq is convergent holds
seq - x is convergent
proof end;

theorem Th9: :: BHSP_2:9
for X being RealUnitarySpace
for seq being sequence of X holds
( seq is convergent iff ex g being Point of X st
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((seq . n) - g).|| < r )
proof end;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
assume A1: seq is convergent ;
func lim seq -> Point of X means :Def2: :: BHSP_2:def 2
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),it) < r;
existence
ex b1 being Point of X st
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),b1) < r
by A1;
uniqueness
for b1, b2 being Point of X st ( for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),b1) < r ) & ( for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),b2) < r ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines lim BHSP_2:def 2 :
for X being RealUnitarySpace
for seq being sequence of X st seq is convergent holds
for b3 being Point of X holds
( b3 = lim seq iff for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),b3) < r );

theorem Th10: :: BHSP_2:10
for X being RealUnitarySpace
for x being Point of X
for seq being sequence of X st seq is constant & x in rng seq holds
lim seq = x
proof end;

theorem :: BHSP_2:11
for X being RealUnitarySpace
for x being Point of X
for seq being sequence of X st seq is constant & ex n being Nat st seq . n = x holds
lim seq = x
proof end;

theorem :: BHSP_2:12
for X being RealUnitarySpace
for seq, seq9 being sequence of X st seq is convergent & ex k being Nat st
for n being Nat st n >= k holds
seq9 . n = seq . n holds
lim seq = lim seq9
proof end;

theorem Th13: :: BHSP_2:13
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
lim (seq1 + seq2) = (lim seq1) + (lim seq2)
proof end;

theorem Th14: :: BHSP_2:14
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
lim (seq1 - seq2) = (lim seq1) - (lim seq2)
proof end;

theorem Th15: :: BHSP_2:15
for X being RealUnitarySpace
for a being Real
for seq being sequence of X st seq is convergent holds
lim (a * seq) = a * (lim seq)
proof end;

theorem Th16: :: BHSP_2:16
for X being RealUnitarySpace
for seq being sequence of X st seq is convergent holds
lim (- seq) = - (lim seq)
proof end;

theorem Th17: :: BHSP_2:17
for X being RealUnitarySpace
for x being Point of X
for seq being sequence of X st seq is convergent holds
lim (seq + x) = (lim seq) + x
proof end;

theorem :: BHSP_2:18
for X being RealUnitarySpace
for x being Point of X
for seq being sequence of X st seq is convergent holds
lim (seq - x) = (lim seq) - x
proof end;

theorem Th19: :: BHSP_2:19
for X being RealUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent holds
( lim seq = g iff for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((seq . n) - g).|| < r )
proof end;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
func ||.seq.|| -> Real_Sequence means :Def3: :: BHSP_2:def 3
for n being Nat holds it . n = ||.(seq . n).||;
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = ||.(seq . n).||
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = ||.(seq . n).|| ) & ( for n being Nat holds b2 . n = ||.(seq . n).|| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines ||. BHSP_2:def 3 :
for X being RealUnitarySpace
for seq being sequence of X
for b3 being Real_Sequence holds
( b3 = ||.seq.|| iff for n being Nat holds b3 . n = ||.(seq . n).|| );

theorem Th20: :: BHSP_2:20
for X being RealUnitarySpace
for seq being sequence of X st seq is convergent holds
||.seq.|| is convergent
proof end;

theorem Th21: :: BHSP_2:21
for X being RealUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.seq.|| is convergent & lim ||.seq.|| = )
proof end;

theorem Th22: :: BHSP_2:22
for X being RealUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )
proof end;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
let x be Point of X;
func dist (seq,x) -> Real_Sequence means :Def4: :: BHSP_2:def 4
for n being Nat holds it . n = dist ((seq . n),x);
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = dist ((seq . n),x)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = dist ((seq . n),x) ) & ( for n being Nat holds b2 . n = dist ((seq . n),x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines dist BHSP_2:def 4 :
for X being RealUnitarySpace
for seq being sequence of X
for x being Point of X
for b4 being Real_Sequence holds
( b4 = dist (seq,x) iff for n being Nat holds b4 . n = dist ((seq . n),x) );

theorem Th23: :: BHSP_2:23
for X being RealUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
dist (seq,g) is convergent
proof end;

theorem Th24: :: BHSP_2:24
for X being RealUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 )
proof end;

theorem :: BHSP_2:25
for X being RealUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.(seq1 + seq2).|| is convergent & lim ||.(seq1 + seq2).|| = ||.(g1 + g2).|| )
proof end;

theorem :: BHSP_2:26
for X being RealUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.((seq1 + seq2) - (g1 + g2)).|| is convergent & lim ||.((seq1 + seq2) - (g1 + g2)).|| = 0 )
proof end;

theorem :: BHSP_2:27
for X being RealUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.(seq1 - seq2).|| is convergent & lim ||.(seq1 - seq2).|| = ||.(g1 - g2).|| )
proof end;

theorem :: BHSP_2:28
for X being RealUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.((seq1 - seq2) - (g1 - g2)).|| is convergent & lim ||.((seq1 - seq2) - (g1 - g2)).|| = 0 )
proof end;

theorem :: BHSP_2:29
for X being RealUnitarySpace
for g being Point of X
for a being Real
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(a * seq).|| is convergent & lim ||.(a * seq).|| = ||.(a * g).|| )
proof end;

theorem :: BHSP_2:30
for X being RealUnitarySpace
for g being Point of X
for a being Real
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((a * seq) - (a * g)).|| is convergent & lim ||.((a * seq) - (a * g)).|| = 0 )
proof end;

theorem :: BHSP_2:31
for X being RealUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| )
proof end;

theorem :: BHSP_2:32
for X being RealUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 )
proof end;

Lm1: for X being RealUnitarySpace
for x, g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )

proof end;

theorem Th33: :: BHSP_2:33
for X being RealUnitarySpace
for x, g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 )
proof end;

theorem :: BHSP_2:34
for X being RealUnitarySpace
for x, g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| )
proof end;

theorem :: BHSP_2:35
for X being RealUnitarySpace
for x, g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 )
proof end;

theorem :: BHSP_2:36
for X being RealUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( dist ((seq1 + seq2),(g1 + g2)) is convergent & lim (dist ((seq1 + seq2),(g1 + g2))) = 0 )
proof end;

theorem :: BHSP_2:37
for X being RealUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( dist ((seq1 - seq2),(g1 - g2)) is convergent & lim (dist ((seq1 - seq2),(g1 - g2))) = 0 )
proof end;

theorem :: BHSP_2:38
for X being RealUnitarySpace
for g being Point of X
for a being Real
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist ((a * seq),(a * g)) is convergent & lim (dist ((a * seq),(a * g))) = 0 )
proof end;

theorem :: BHSP_2:39
for X being RealUnitarySpace
for x, g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist ((seq + x),(g + x)) is convergent & lim (dist ((seq + x),(g + x))) = 0 )
proof end;

definition
let X be RealUnitarySpace;
let x be Point of X;
let r be Real;
func Ball (x,r) -> Subset of X equals :: BHSP_2:def 5
{ y where y is Point of X : ||.(x - y).|| < r } ;
coherence
{ y where y is Point of X : ||.(x - y).|| < r } is Subset of X
proof end;
func cl_Ball (x,r) -> Subset of X equals :: BHSP_2:def 6
{ y where y is Point of X : ||.(x - y).|| <= r } ;
coherence
{ y where y is Point of X : ||.(x - y).|| <= r } is Subset of X
proof end;
func Sphere (x,r) -> Subset of X equals :: BHSP_2:def 7
{ y where y is Point of X : ||.(x - y).|| = r } ;
coherence
{ y where y is Point of X : ||.(x - y).|| = r } is Subset of X
proof end;
end;

:: deftheorem defines Ball BHSP_2:def 5 :
for X being RealUnitarySpace
for x being Point of X
for r being Real holds Ball (x,r) = { y where y is Point of X : ||.(x - y).|| < r } ;

:: deftheorem defines cl_Ball BHSP_2:def 6 :
for X being RealUnitarySpace
for x being Point of X
for r being Real holds cl_Ball (x,r) = { y where y is Point of X : ||.(x - y).|| <= r } ;

:: deftheorem defines Sphere BHSP_2:def 7 :
for X being RealUnitarySpace
for x being Point of X
for r being Real holds Sphere (x,r) = { y where y is Point of X : ||.(x - y).|| = r } ;

theorem Th40: :: BHSP_2:40
for X being RealUnitarySpace
for x, z being Point of X
for r being Real holds
( z in Ball (x,r) iff ||.(x - z).|| < r )
proof end;

theorem Th41: :: BHSP_2:41
for X being RealUnitarySpace
for x, z being Point of X
for r being Real holds
( z in Ball (x,r) iff dist (x,z) < r )
proof end;

theorem :: BHSP_2:42
for X being RealUnitarySpace
for x being Point of X
for r being Real st r > 0 holds
x in Ball (x,r)
proof end;

theorem :: BHSP_2:43
for X being RealUnitarySpace
for x, y, z being Point of X
for r being Real st y in Ball (x,r) & z in Ball (x,r) holds
dist (y,z) < 2 * r
proof end;

theorem :: BHSP_2:44
for X being RealUnitarySpace
for x, y, z being Point of X
for r being Real st y in Ball (x,r) holds
y - z in Ball ((x - z),r)
proof end;

theorem :: BHSP_2:45
for X being RealUnitarySpace
for x, y being Point of X
for r being Real st y in Ball (x,r) holds
y - x in Ball ((0. X),r)
proof end;

theorem :: BHSP_2:46
for X being RealUnitarySpace
for x, y being Point of X
for q, r being Real st y in Ball (x,r) & r <= q holds
y in Ball (x,q)
proof end;

theorem Th47: :: BHSP_2:47
for X being RealUnitarySpace
for x, z being Point of X
for r being Real holds
( z in cl_Ball (x,r) iff ||.(x - z).|| <= r )
proof end;

theorem Th48: :: BHSP_2:48
for X being RealUnitarySpace
for x, z being Point of X
for r being Real holds
( z in cl_Ball (x,r) iff dist (x,z) <= r )
proof end;

theorem :: BHSP_2:49
for X being RealUnitarySpace
for x being Point of X
for r being Real st r >= 0 holds
x in cl_Ball (x,r)
proof end;

theorem Th50: :: BHSP_2:50
for X being RealUnitarySpace
for x, y being Point of X
for r being Real st y in Ball (x,r) holds
y in cl_Ball (x,r)
proof end;

theorem Th51: :: BHSP_2:51
for X being RealUnitarySpace
for x, z being Point of X
for r being Real holds
( z in Sphere (x,r) iff ||.(x - z).|| = r )
proof end;

theorem :: BHSP_2:52
for X being RealUnitarySpace
for x, z being Point of X
for r being Real holds
( z in Sphere (x,r) iff dist (x,z) = r )
proof end;

theorem :: BHSP_2:53
for X being RealUnitarySpace
for x, y being Point of X
for r being Real st y in Sphere (x,r) holds
y in cl_Ball (x,r)
proof end;

theorem Th54: :: BHSP_2:54
for X being RealUnitarySpace
for x being Point of X
for r being Real holds Ball (x,r) c= cl_Ball (x,r)
proof end;

theorem Th55: :: BHSP_2:55
for X being RealUnitarySpace
for x being Point of X
for r being Real holds Sphere (x,r) c= cl_Ball (x,r)
proof end;

theorem :: BHSP_2:56
for X being RealUnitarySpace
for x being Point of X
for r being Real holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)
proof end;