:: by Noboru Endou

::

:: Received February 10, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

deffunc H

:: deftheorem defines convergent CLVECT_2:def 1 :

for X being ComplexUnitarySpace

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 );

for X being ComplexUnitarySpace

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 );

theorem Th1: :: CLVECT_2:1

for X being ComplexUnitarySpace

for seq being sequence of X st seq is constant holds

seq is convergent

for seq being sequence of X st seq is constant holds

seq is convergent

proof end;

theorem Th2: :: CLVECT_2:2

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st seq1 is convergent & ex k being Nat st

for n being Nat st k <= n holds

seq2 . n = seq1 . n holds

seq2 is convergent

for seq1, seq2 being sequence of X st seq1 is convergent & ex k being Nat st

for n being Nat st k <= n holds

seq2 . n = seq1 . n holds

seq2 is convergent

proof end;

theorem Th3: :: CLVECT_2:3

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds

seq1 + seq2 is convergent

for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds

seq1 + seq2 is convergent

proof end;

theorem Th4: :: CLVECT_2:4

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds

seq1 - seq2 is convergent

for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds

seq1 - seq2 is convergent

proof end;

theorem Th5: :: CLVECT_2:5

for X being ComplexUnitarySpace

for z being Complex

for seq being sequence of X st seq is convergent holds

z * seq is convergent

for z being Complex

for seq being sequence of X st seq is convergent holds

z * seq is convergent

proof end;

theorem Th6: :: CLVECT_2:6

for X being ComplexUnitarySpace

for seq being sequence of X st seq is convergent holds

- seq is convergent

for seq being sequence of X st seq is convergent holds

- seq is convergent

proof end;

theorem Th7: :: CLVECT_2:7

for X being ComplexUnitarySpace

for x being Point of X

for seq being sequence of X st seq is convergent holds

seq + x is convergent

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: :: CLVECT_2:8

for X being ComplexUnitarySpace

for x being Point of X

for seq being sequence of X st seq is convergent holds

seq - x is convergent

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: :: CLVECT_2:9

for X being ComplexUnitarySpace

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 )

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 ComplexUnitarySpace;

let seq be sequence of X;

assume A1: seq is convergent ;

ex b_{1} 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),b_{1}) < r
by A1;

uniqueness

for b_{1}, b_{2} 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),b_{1}) < 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),b_{2}) < r ) holds

b_{1} = b_{2}

end;
let seq be sequence of X;

assume A1: seq is convergent ;

func lim seq -> Point of X means :Def2: :: CLVECT_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 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;

ex b

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),b

uniqueness

for b

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),b

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),b

b

proof end;

:: deftheorem Def2 defines lim CLVECT_2:def 2 :

for X being ComplexUnitarySpace

for seq being sequence of X st seq is convergent holds

for b_{3} being Point of X holds

( b_{3} = 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),b_{3}) < r );

for X being ComplexUnitarySpace

for seq being sequence of X st seq is convergent holds

for b

( b

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),b

theorem Th10: :: CLVECT_2:10

for X being ComplexUnitarySpace

for x being Point of X

for seq being sequence of X st seq is constant & x in rng seq holds

lim seq = x

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 :: CLVECT_2:11

for X being ComplexUnitarySpace

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

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 :: CLVECT_2:12

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st seq1 is convergent & ex k being Nat st

for n being Nat st n >= k holds

seq2 . n = seq1 . n holds

lim seq1 = lim seq2

for seq1, seq2 being sequence of X st seq1 is convergent & ex k being Nat st

for n being Nat st n >= k holds

seq2 . n = seq1 . n holds

lim seq1 = lim seq2

proof end;

theorem Th13: :: CLVECT_2:13

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds

lim (seq1 + seq2) = (lim seq1) + (lim seq2)

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: :: CLVECT_2:14

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds

lim (seq1 - seq2) = (lim seq1) - (lim seq2)

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: :: CLVECT_2:15

for X being ComplexUnitarySpace

for z being Complex

for seq being sequence of X st seq is convergent holds

lim (z * seq) = z * (lim seq)

for z being Complex

for seq being sequence of X st seq is convergent holds

lim (z * seq) = z * (lim seq)

proof end;

theorem Th16: :: CLVECT_2:16

for X being ComplexUnitarySpace

for seq being sequence of X st seq is convergent holds

lim (- seq) = - (lim seq)

for seq being sequence of X st seq is convergent holds

lim (- seq) = - (lim seq)

proof end;

theorem Th17: :: CLVECT_2:17

for X being ComplexUnitarySpace

for x being Point of X

for seq being sequence of X st seq is convergent holds

lim (seq + x) = (lim seq) + x

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 :: CLVECT_2:18

for X being ComplexUnitarySpace

for x being Point of X

for seq being sequence of X st seq is convergent holds

lim (seq - x) = (lim seq) - x

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: :: CLVECT_2:19

for X being ComplexUnitarySpace

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 )

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 ComplexUnitarySpace;

let seq be sequence of X;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = ||.(seq . n).||

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = ||.(seq . n).|| ) & ( for n being Nat holds b_{2} . n = ||.(seq . n).|| ) holds

b_{1} = b_{2}

end;
let seq be sequence of X;

func ||.seq.|| -> Real_Sequence means :Def3: :: CLVECT_2:def 3

for n being Nat holds it . n = ||.(seq . n).||;

existence for n being Nat holds it . n = ||.(seq . n).||;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines ||. CLVECT_2:def 3 :

for X being ComplexUnitarySpace

for seq being sequence of X

for b_{3} being Real_Sequence holds

( b_{3} = ||.seq.|| iff for n being Nat holds b_{3} . n = ||.(seq . n).|| );

for X being ComplexUnitarySpace

for seq being sequence of X

for b

( b

theorem Th20: :: CLVECT_2:20

for X being ComplexUnitarySpace

for seq being sequence of X st seq is convergent holds

||.seq.|| is convergent

for seq being sequence of X st seq is convergent holds

||.seq.|| is convergent

proof end;

theorem Th21: :: CLVECT_2:21

for X being ComplexUnitarySpace

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.|| )

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 Th22: :: CLVECT_2:22

for X being ComplexUnitarySpace

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 )

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 ComplexUnitarySpace;

let seq be sequence of X;

let x be Point of X;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = dist ((seq . n),x)

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = dist ((seq . n),x) ) & ( for n being Nat holds b_{2} . n = dist ((seq . n),x) ) holds

b_{1} = b_{2}

end;
let seq be sequence of X;

let x be Point of X;

func dist (seq,x) -> Real_Sequence means :Def4: :: CLVECT_2:def 4

for n being Nat holds it . n = dist ((seq . n),x);

existence for n being Nat holds it . n = dist ((seq . n),x);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines dist CLVECT_2:def 4 :

for X being ComplexUnitarySpace

for seq being sequence of X

for x being Point of X

for b_{4} being Real_Sequence holds

( b_{4} = dist (seq,x) iff for n being Nat holds b_{4} . n = dist ((seq . n),x) );

for X being ComplexUnitarySpace

for seq being sequence of X

for x being Point of X

for b

( b

theorem Th23: :: CLVECT_2:23

for X being ComplexUnitarySpace

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

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: :: CLVECT_2:24

for X being ComplexUnitarySpace

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 )

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 :: CLVECT_2:25

for X being ComplexUnitarySpace

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).|| )

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 :: CLVECT_2:26

for X being ComplexUnitarySpace

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 )

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 :: CLVECT_2:27

for X being ComplexUnitarySpace

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).|| )

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 :: CLVECT_2:28

for X being ComplexUnitarySpace

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 )

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 :: CLVECT_2:29

for X being ComplexUnitarySpace

for g being Point of X

for z being Complex

for seq being sequence of X st seq is convergent & lim seq = g holds

( ||.(z * seq).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| )

for g being Point of X

for z being Complex

for seq being sequence of X st seq is convergent & lim seq = g holds

( ||.(z * seq).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| )

proof end;

theorem :: CLVECT_2:30

for X being ComplexUnitarySpace

for g being Point of X

for z being Complex

for seq being sequence of X st seq is convergent & lim seq = g holds

( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 )

for g being Point of X

for z being Complex

for seq being sequence of X st seq is convergent & lim seq = g holds

( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 )

proof end;

theorem :: CLVECT_2:31

for X being ComplexUnitarySpace

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).|| )

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 :: CLVECT_2:32

for X being ComplexUnitarySpace

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 )

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 ComplexUnitarySpace

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: :: CLVECT_2:33

for X being ComplexUnitarySpace

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 )

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 :: CLVECT_2:34

for X being ComplexUnitarySpace

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).|| )

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 :: CLVECT_2:35

for X being ComplexUnitarySpace

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 )

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 :: CLVECT_2:36

for X being ComplexUnitarySpace

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 )

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 :: CLVECT_2:37

for X being ComplexUnitarySpace

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 )

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 :: CLVECT_2:38

for X being ComplexUnitarySpace

for g being Point of X

for z being Complex

for seq being sequence of X st seq is convergent & lim seq = g holds

( dist ((z * seq),(z * g)) is convergent & lim (dist ((z * seq),(z * g))) = 0 )

for g being Point of X

for z being Complex

for seq being sequence of X st seq is convergent & lim seq = g holds

( dist ((z * seq),(z * g)) is convergent & lim (dist ((z * seq),(z * g))) = 0 )

proof end;

theorem :: CLVECT_2:39

for X being ComplexUnitarySpace

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 )

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 ComplexUnitarySpace;

let x be Point of X;

let r be Real;

{ y where y is Point of X : ||.(x - y).|| < r } is Subset of X

{ y where y is Point of X : ||.(x - y).|| <= r } is Subset of X

{ y where y is Point of X : ||.(x - y).|| = r } is Subset of X

end;
let x be Point of X;

let r be Real;

func Ball (x,r) -> Subset of X equals :: CLVECT_2:def 5

{ y where y is Point of X : ||.(x - y).|| < r } ;

coherence { y where y is Point of X : ||.(x - y).|| < r } ;

{ 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 :: CLVECT_2:def 6

{ y where y is Point of X : ||.(x - y).|| <= r } ;

coherence { y where y is Point of X : ||.(x - y).|| <= r } ;

{ y where y is Point of X : ||.(x - y).|| <= r } is Subset of X

proof end;

func Sphere (x,r) -> Subset of X equals :: CLVECT_2:def 7

{ y where y is Point of X : ||.(x - y).|| = r } ;

coherence { y where y is Point of X : ||.(x - y).|| = r } ;

{ y where y is Point of X : ||.(x - y).|| = r } is Subset of X

proof end;

:: deftheorem defines Ball CLVECT_2:def 5 :

for X being ComplexUnitarySpace

for x being Point of X

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

for X being ComplexUnitarySpace

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 CLVECT_2:def 6 :

for X being ComplexUnitarySpace

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 } ;

for X being ComplexUnitarySpace

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 CLVECT_2:def 7 :

for X being ComplexUnitarySpace

for x being Point of X

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

for X being ComplexUnitarySpace

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: :: CLVECT_2:40

for X being ComplexUnitarySpace

for x, w being Point of X

for r being Real holds

( w in Ball (x,r) iff ||.(x - w).|| < r )

for x, w being Point of X

for r being Real holds

( w in Ball (x,r) iff ||.(x - w).|| < r )

proof end;

theorem Th41: :: CLVECT_2:41

for X being ComplexUnitarySpace

for x, w being Point of X

for r being Real holds

( w in Ball (x,r) iff dist (x,w) < r )

for x, w being Point of X

for r being Real holds

( w in Ball (x,r) iff dist (x,w) < r )

proof end;

theorem :: CLVECT_2:42

for X being ComplexUnitarySpace

for x being Point of X

for r being Real st r > 0 holds

x in Ball (x,r)

for x being Point of X

for r being Real st r > 0 holds

x in Ball (x,r)

proof end;

theorem :: CLVECT_2:43

for X being ComplexUnitarySpace

for x, y, w being Point of X

for r being Real st y in Ball (x,r) & w in Ball (x,r) holds

dist (y,w) < 2 * r

for x, y, w being Point of X

for r being Real st y in Ball (x,r) & w in Ball (x,r) holds

dist (y,w) < 2 * r

proof end;

theorem :: CLVECT_2:44

for X being ComplexUnitarySpace

for x, y, w being Point of X

for r being Real st y in Ball (x,r) holds

y - w in Ball ((x - w),r)

for x, y, w being Point of X

for r being Real st y in Ball (x,r) holds

y - w in Ball ((x - w),r)

proof end;

theorem :: CLVECT_2:45

for X being ComplexUnitarySpace

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)

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 :: CLVECT_2:46

for X being ComplexUnitarySpace

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)

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: :: CLVECT_2:47

for X being ComplexUnitarySpace

for x, w being Point of X

for r being Real holds

( w in cl_Ball (x,r) iff ||.(x - w).|| <= r )

for x, w being Point of X

for r being Real holds

( w in cl_Ball (x,r) iff ||.(x - w).|| <= r )

proof end;

theorem Th48: :: CLVECT_2:48

for X being ComplexUnitarySpace

for x, w being Point of X

for r being Real holds

( w in cl_Ball (x,r) iff dist (x,w) <= r )

for x, w being Point of X

for r being Real holds

( w in cl_Ball (x,r) iff dist (x,w) <= r )

proof end;

theorem :: CLVECT_2:49

for X being ComplexUnitarySpace

for x being Point of X

for r being Real st r >= 0 holds

x in cl_Ball (x,r)

for x being Point of X

for r being Real st r >= 0 holds

x in cl_Ball (x,r)

proof end;

theorem Th50: :: CLVECT_2:50

for X being ComplexUnitarySpace

for x, y being Point of X

for r being Real st y in Ball (x,r) holds

y in cl_Ball (x,r)

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: :: CLVECT_2:51

for X being ComplexUnitarySpace

for x, w being Point of X

for r being Real holds

( w in Sphere (x,r) iff ||.(x - w).|| = r )

for x, w being Point of X

for r being Real holds

( w in Sphere (x,r) iff ||.(x - w).|| = r )

proof end;

theorem :: CLVECT_2:52

for X being ComplexUnitarySpace

for x, w being Point of X

for r being Real holds

( w in Sphere (x,r) iff dist (x,w) = r )

for x, w being Point of X

for r being Real holds

( w in Sphere (x,r) iff dist (x,w) = r )

proof end;

theorem :: CLVECT_2:53

for X being ComplexUnitarySpace

for x, y being Point of X

for r being Real st y in Sphere (x,r) holds

y in cl_Ball (x,r)

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: :: CLVECT_2:54

for X being ComplexUnitarySpace

for x being Point of X

for r being Real holds Ball (x,r) c= cl_Ball (x,r)

for x being Point of X

for r being Real holds Ball (x,r) c= cl_Ball (x,r)

proof end;

theorem Th55: :: CLVECT_2:55

for X being ComplexUnitarySpace

for x being Point of X

for r being Real holds Sphere (x,r) c= cl_Ball (x,r)

for x being Point of X

for r being Real holds Sphere (x,r) c= cl_Ball (x,r)

proof end;

theorem :: CLVECT_2:56

for X being ComplexUnitarySpace

for x being Point of X

for r being Real holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)

for x being Point of X

for r being Real holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)

proof end;

deffunc H

:: deftheorem defines Cauchy CLVECT_2:def 8 :

for X being ComplexUnitarySpace

for seq being sequence of X holds

( seq is Cauchy iff for r being Real st r > 0 holds

ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

dist ((seq . n),(seq . m)) < r );

for X being ComplexUnitarySpace

for seq being sequence of X holds

( seq is Cauchy iff for r being Real st r > 0 holds

ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

dist ((seq . n),(seq . m)) < r );

theorem :: CLVECT_2:58

for X being ComplexUnitarySpace

for seq being sequence of X holds

( seq is Cauchy iff for r being Real st r > 0 holds

ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < r )

for seq being sequence of X holds

( seq is Cauchy iff for r being Real st r > 0 holds

ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < r )

proof end;

theorem :: CLVECT_2:59

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds

seq1 + seq2 is Cauchy

for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds

seq1 + seq2 is Cauchy

proof end;

theorem :: CLVECT_2:60

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds

seq1 - seq2 is Cauchy

for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds

seq1 - seq2 is Cauchy

proof end;

theorem Th61: :: CLVECT_2:61

for X being ComplexUnitarySpace

for z being Complex

for seq being sequence of X st seq is Cauchy holds

z * seq is Cauchy

for z being Complex

for seq being sequence of X st seq is Cauchy holds

z * seq is Cauchy

proof end;

theorem Th63: :: CLVECT_2:63

for X being ComplexUnitarySpace

for x being Point of X

for seq being sequence of X st seq is Cauchy holds

seq + x is Cauchy

for x being Point of X

for seq being sequence of X st seq is Cauchy holds

seq + x is Cauchy

proof end;

theorem :: CLVECT_2:64

for X being ComplexUnitarySpace

for x being Point of X

for seq being sequence of X st seq is Cauchy holds

seq - x is Cauchy

for x being Point of X

for seq being sequence of X st seq is Cauchy holds

seq - x is Cauchy

proof end;

theorem :: CLVECT_2:65

for X being ComplexUnitarySpace

for seq being sequence of X st seq is convergent holds

seq is Cauchy

for seq being sequence of X st seq is convergent holds

seq is Cauchy

proof end;

:: deftheorem defines is_compared_to CLVECT_2:def 9 :

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X holds

( seq1 is_compared_to seq2 iff for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq1 . n),(seq2 . n)) < r );

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X holds

( seq1 is_compared_to seq2 iff for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq1 . n),(seq2 . n)) < r );

theorem Th67: :: CLVECT_2:67

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st seq1 is_compared_to seq2 holds

seq2 is_compared_to seq1

for seq1, seq2 being sequence of X st seq1 is_compared_to seq2 holds

seq2 is_compared_to seq1

proof end;

definition

let X be ComplexUnitarySpace;

let seq1, seq2 be sequence of X;

:: original: is_compared_to

redefine pred seq1 is_compared_to seq2;

reflexivity

for seq1 being sequence of X holds (X,b_{1},b_{1})
by Th66;

symmetry

for seq1, seq2 being sequence of X st (X,b_{1},b_{2}) holds

(X,b_{2},b_{1})
by Th67;

end;
let seq1, seq2 be sequence of X;

:: original: is_compared_to

redefine pred seq1 is_compared_to seq2;

reflexivity

for seq1 being sequence of X holds (X,b

symmetry

for seq1, seq2 being sequence of X st (X,b

(X,b

theorem :: CLVECT_2:68

for X being ComplexUnitarySpace

for seq1, seq2, seq3 being sequence of X st seq1 is_compared_to seq2 & seq2 is_compared_to seq3 holds

seq1 is_compared_to seq3

for seq1, seq2, seq3 being sequence of X st seq1 is_compared_to seq2 & seq2 is_compared_to seq3 holds

seq1 is_compared_to seq3

proof end;

theorem :: CLVECT_2:69

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X holds

( seq1 is_compared_to seq2 iff for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq1 . n) - (seq2 . n)).|| < r )

for seq1, seq2 being sequence of X holds

( seq1 is_compared_to seq2 iff for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

||.((seq1 . n) - (seq2 . n)).|| < r )

proof end;

theorem :: CLVECT_2:70

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st ex k being Nat st

for n being Nat st n >= k holds

seq1 . n = seq2 . n holds

seq1 is_compared_to seq2

for seq1, seq2 being sequence of X st ex k being Nat st

for n being Nat st n >= k holds

seq1 . n = seq2 . n holds

seq1 is_compared_to seq2

proof end;

theorem :: CLVECT_2:71

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st seq1 is Cauchy & seq1 is_compared_to seq2 holds

seq2 is Cauchy

for seq1, seq2 being sequence of X st seq1 is Cauchy & seq1 is_compared_to seq2 holds

seq2 is Cauchy

proof end;

theorem :: CLVECT_2:72

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st seq1 is convergent & seq1 is_compared_to seq2 holds

seq2 is convergent

for seq1, seq2 being sequence of X st seq1 is convergent & seq1 is_compared_to seq2 holds

seq2 is convergent

proof end;

theorem :: CLVECT_2:73

for X being ComplexUnitarySpace

for g being Point of X

for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 holds

( seq2 is convergent & lim seq2 = g )

for g being Point of X

for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 holds

( seq2 is convergent & lim seq2 = g )

proof end;

:: deftheorem defines bounded CLVECT_2:def 10 :

for X being ComplexUnitarySpace

for seq being sequence of X holds

( seq is bounded iff ex M being Real st

( M > 0 & ( for n being Nat holds ||.(seq . n).|| <= M ) ) );

for X being ComplexUnitarySpace

for seq being sequence of X holds

( seq is bounded iff ex M being Real st

( M > 0 & ( for n being Nat holds ||.(seq . n).|| <= M ) ) );

theorem Th74: :: CLVECT_2:74

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds

seq1 + seq2 is bounded

for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds

seq1 + seq2 is bounded

proof end;

theorem Th75: :: CLVECT_2:75

for X being ComplexUnitarySpace

for seq being sequence of X st seq is bounded holds

- seq is bounded

for seq being sequence of X st seq is bounded holds

- seq is bounded

proof end;

theorem :: CLVECT_2:76

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds

seq1 - seq2 is bounded

for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds

seq1 - seq2 is bounded

proof end;

theorem :: CLVECT_2:77

for X being ComplexUnitarySpace

for z being Complex

for seq being sequence of X st seq is bounded holds

z * seq is bounded

for z being Complex

for seq being sequence of X st seq is bounded holds

z * seq is bounded

proof end;

theorem Th79: :: CLVECT_2:79

for X being ComplexUnitarySpace

for seq being sequence of X

for m being Nat ex M being Real st

( M > 0 & ( for n being Nat st n <= m holds

||.(seq . n).|| < M ) )

for seq being sequence of X

for m being Nat ex M being Real st

( M > 0 & ( for n being Nat st n <= m holds

||.(seq . n).|| < M ) )

proof end;

theorem Th80: :: CLVECT_2:80

for X being ComplexUnitarySpace

for seq being sequence of X st seq is convergent holds

seq is bounded

for seq being sequence of X st seq is convergent holds

seq is bounded

proof end;

theorem :: CLVECT_2:81

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X st seq1 is bounded & seq1 is_compared_to seq2 holds

seq2 is bounded

for seq1, seq2 being sequence of X st seq1 is bounded & seq1 is_compared_to seq2 holds

seq2 is bounded

proof end;

theorem Th82: :: CLVECT_2:82

for X being ComplexUnitarySpace

for seq, seq1 being sequence of X st seq is bounded & seq1 is subsequence of seq holds

seq1 is bounded

for seq, seq1 being sequence of X st seq is bounded & seq1 is subsequence of seq holds

seq1 is bounded

proof end;

theorem Th83: :: CLVECT_2:83

for X being ComplexUnitarySpace

for seq, seq1 being sequence of X st seq is convergent & seq1 is subsequence of seq holds

seq1 is convergent

for seq, seq1 being sequence of X st seq is convergent & seq1 is subsequence of seq holds

seq1 is convergent

proof end;

theorem Th84: :: CLVECT_2:84

for X being ComplexUnitarySpace

for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds

lim seq1 = lim seq

for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds

lim seq1 = lim seq

proof end;

theorem Th85: :: CLVECT_2:85

for X being ComplexUnitarySpace

for seq, seq1 being sequence of X st seq is Cauchy & seq1 is subsequence of seq holds

seq1 is Cauchy

for seq, seq1 being sequence of X st seq is Cauchy & seq1 is subsequence of seq holds

seq1 is Cauchy

proof end;

theorem Th86: :: CLVECT_2:86

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X

for k being Nat holds (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k)

for seq1, seq2 being sequence of X

for k being Nat holds (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k)

proof end;

theorem Th87: :: CLVECT_2:87

for X being ComplexUnitarySpace

for seq being sequence of X

for k being Nat holds (- seq) ^\ k = - (seq ^\ k)

for seq being sequence of X

for k being Nat holds (- seq) ^\ k = - (seq ^\ k)

proof end;

theorem :: CLVECT_2:88

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X

for k being Nat holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)

for seq1, seq2 being sequence of X

for k being Nat holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)

proof end;

theorem :: CLVECT_2:89

for X being ComplexUnitarySpace

for z being Complex

for seq being sequence of X

for k being Nat holds (z * seq) ^\ k = z * (seq ^\ k)

for z being Complex

for seq being sequence of X

for k being Nat holds (z * seq) ^\ k = z * (seq ^\ k)

proof end;

theorem :: CLVECT_2:90

for X being ComplexUnitarySpace

for seq being sequence of X

for k being Nat st seq is convergent holds

( seq ^\ k is convergent & lim (seq ^\ k) = lim seq ) by Th83, Th84;

for seq being sequence of X

for k being Nat st seq is convergent holds

( seq ^\ k is convergent & lim (seq ^\ k) = lim seq ) by Th83, Th84;

theorem :: CLVECT_2:91

for X being ComplexUnitarySpace

for seq, seq1 being sequence of X st seq is convergent & ex k being Nat st seq = seq1 ^\ k holds

seq1 is convergent

for seq, seq1 being sequence of X st seq is convergent & ex k being Nat st seq = seq1 ^\ k holds

seq1 is convergent

proof end;

theorem :: CLVECT_2:92

for X being ComplexUnitarySpace

for seq, seq1 being sequence of X st seq is Cauchy & ex k being Nat st seq = seq1 ^\ k holds

seq1 is Cauchy

for seq, seq1 being sequence of X st seq is Cauchy & ex k being Nat st seq = seq1 ^\ k holds

seq1 is Cauchy

proof end;

theorem :: CLVECT_2:93

theorem :: CLVECT_2:94

for X being ComplexUnitarySpace

for seq1, seq2 being sequence of X

for k being Nat st seq1 is_compared_to seq2 holds

seq1 ^\ k is_compared_to seq2 ^\ k

for seq1, seq2 being sequence of X

for k being Nat st seq1 is_compared_to seq2 holds

seq1 ^\ k is_compared_to seq2 ^\ k

proof end;

theorem :: CLVECT_2:95

theorem :: CLVECT_2:96

definition

let X be ComplexUnitarySpace;

end;
attr X is complete means :: CLVECT_2:def 11

for seq being sequence of X st seq is Cauchy holds

seq is convergent ;

for seq being sequence of X st seq is Cauchy holds

seq is convergent ;

:: deftheorem defines complete CLVECT_2:def 11 :

for X being ComplexUnitarySpace holds

( X is complete iff for seq being sequence of X st seq is Cauchy holds

seq is convergent );

for X being ComplexUnitarySpace holds

( X is complete iff for seq being sequence of X st seq is Cauchy holds

seq is convergent );

theorem :: CLVECT_2:97