:: by Jan Popio{\l}ek

::

:: Received July 19, 1991

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

deffunc H

registration

let X be RealUnitarySpace;

ex b_{1} being sequence of X st b_{1} is constant

end;
cluster V1() V4( NAT ) V5( the U1 of X) V6() constant V11() V14( NAT ) V18( NAT , the U1 of X) for Element of K19(K20(NAT, the U1 of X));

existence ex b

proof end;

:: deftheorem Def1 defines Cauchy BHSP_3:def 1 :

for X being RealUnitarySpace

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 RealUnitarySpace

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

registration

let X be RealUnitarySpace;

coherence

for b_{1} being sequence of X st b_{1} is constant holds

b_{1} is Cauchy

end;
coherence

for b

b

proof end;

::$CT

theorem :: BHSP_3:2

for X being RealUnitarySpace

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;

registration

let X be RealUnitarySpace;

let seq1, seq2 be Cauchy sequence of X;

coherence

seq1 + seq2 is Cauchy

end;
let seq1, seq2 be Cauchy sequence of X;

coherence

seq1 + seq2 is Cauchy

proof end;

registration

let X be RealUnitarySpace;

let seq1, seq2 be Cauchy sequence of X;

coherence

seq1 - seq2 is Cauchy

end;
let seq1, seq2 be Cauchy sequence of X;

coherence

seq1 - seq2 is Cauchy

proof end;

registration

let X be RealUnitarySpace;

let a be Real;

let seq be Cauchy sequence of X;

coherence

a * seq is Cauchy

end;
let a be Real;

let seq be Cauchy sequence of X;

coherence

a * seq is Cauchy

proof end;

registration
end;

registration

let X be RealUnitarySpace;

let x be Point of X;

let seq be Cauchy sequence of X;

coherence

seq + x is Cauchy

end;
let x be Point of X;

let seq be Cauchy sequence of X;

coherence

seq + x is Cauchy

proof end;

registration

let X be RealUnitarySpace;

let x be Point of X;

let seq be Cauchy sequence of X;

coherence

seq - x is Cauchy

end;
let x be Point of X;

let seq be Cauchy sequence of X;

coherence

seq - x is Cauchy

proof end;

registration

let X be RealUnitarySpace;

for b_{1} being sequence of X st b_{1} is convergent holds

b_{1} is Cauchy

end;
cluster V6() V18( NAT , the U1 of X) convergent -> Cauchy for Element of K19(K20(NAT, the U1 of X));

coherence for b

b

proof end;

definition

let X be RealUnitarySpace;

let seq1, seq2 be sequence of X;

for seq1 being sequence of X

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

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

for seq1, seq2 being sequence 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 ((seq1 . n),(seq2 . n)) < r ) holds

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

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

end;
let seq1, seq2 be sequence of X;

pred seq1 is_compared_to seq2 means :: BHSP_3:def 2

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;

reflexivity 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 seq1 being sequence of X

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

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

proof end;

symmetry for seq1, seq2 being sequence 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 ((seq1 . n),(seq2 . n)) < r ) holds

for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

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

proof end;

:: deftheorem defines is_compared_to BHSP_3:def 2 :

for X being RealUnitarySpace

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 RealUnitarySpace

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

::$CT 9

theorem :: BHSP_3:12

for X being RealUnitarySpace

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 :: BHSP_3:13

for X being RealUnitarySpace

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

for X being RealUnitarySpace

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

for X being RealUnitarySpace

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 :: BHSP_3:16

for X being RealUnitarySpace

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 :: BHSP_3:17

for X being RealUnitarySpace

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 Def3 defines bounded BHSP_3:def 3 :

for X being RealUnitarySpace

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 RealUnitarySpace

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

registration

let X be RealUnitarySpace;

coherence

for b_{1} being sequence of X st b_{1} is constant holds

b_{1} is bounded

end;
coherence

for b

b

proof end;

registration

let X be RealUnitarySpace;

let seq1, seq2 be bounded sequence of X;

coherence

seq1 + seq2 is bounded

end;
let seq1, seq2 be bounded sequence of X;

coherence

seq1 + seq2 is bounded

proof end;

registration
end;

registration

let X be RealUnitarySpace;

let seq1, seq2 be bounded sequence of X;

coherence

seq1 - seq2 is bounded

end;
let seq1, seq2 be bounded sequence of X;

coherence

seq1 - seq2 is bounded

proof end;

registration

let X be RealUnitarySpace;

let a be Real;

let seq be bounded sequence of X;

coherence

a * seq is bounded

end;
let a be Real;

let seq be bounded sequence of X;

coherence

a * seq is bounded

proof end;

::$CT 5

theorem Th8: :: BHSP_3:23

for X being RealUnitarySpace

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;

registration

let X be RealUnitarySpace;

for b_{1} being sequence of X st b_{1} is convergent holds

b_{1} is bounded

end;
cluster V6() V18( NAT , the U1 of X) convergent -> bounded for Element of K19(K20(NAT, the U1 of X));

coherence for b

b

proof end;

::$CT

theorem :: BHSP_3:25

for X being RealUnitarySpace

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;

registration

let X be RealUnitarySpace;

let seq be bounded sequence of X;

coherence

for b_{1} being subsequence of seq holds b_{1} is bounded

end;
let seq be bounded sequence of X;

coherence

for b

proof end;

registration

let X be RealUnitarySpace;

let seq be convergent sequence of X;

coherence

for b_{1} being subsequence of seq holds b_{1} is convergent

end;
let seq be convergent sequence of X;

coherence

for b

proof end;

::$CT 2

theorem Th10: :: BHSP_3:28

for X being RealUnitarySpace

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;

registration

let X be RealUnitarySpace;

let seq be Cauchy sequence of X;

coherence

for b_{1} being subsequence of seq holds b_{1} is Cauchy

end;
let seq be Cauchy sequence of X;

coherence

for b

proof end;

::$CT

theorem :: BHSP_3:30

for X being RealUnitarySpace

for seq being sequence of X

for k, m being Nat holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k

for seq being sequence of X

for k, m being Nat holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k

proof end;

theorem :: BHSP_3:31

for X being RealUnitarySpace

for seq being sequence of X

for k, m being Nat holds (seq ^\ k) ^\ m = seq ^\ (k + m)

for seq being sequence of X

for k, m being Nat holds (seq ^\ k) ^\ m = seq ^\ (k + m)

proof end;

theorem Th13: :: BHSP_3:32

for X being RealUnitarySpace

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 Th14: :: BHSP_3:33

for X being RealUnitarySpace

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

for X being RealUnitarySpace

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

for X being RealUnitarySpace

for a being Real

for seq being sequence of X

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

for a being Real

for seq being sequence of X

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

proof end;

theorem :: BHSP_3:36

for X being RealUnitarySpace

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

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

theorem :: BHSP_3:37

for X being RealUnitarySpace

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

for X being RealUnitarySpace

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;

::$CT

theorem :: BHSP_3:40

for X being RealUnitarySpace

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;

definition

let X be RealUnitarySpace;

end;
attr X is complete means :: BHSP_3:def 4

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 BHSP_3:def 4 :

for X being RealUnitarySpace holds

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

seq is convergent );

for X being RealUnitarySpace holds

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

seq is convergent );

::$CT 2

theorem :: BHSP_3:43

for X being RealUnitarySpace

for seq being sequence of X st X is complete & seq is Cauchy holds

seq is bounded

for seq being sequence of X st X is complete & seq is Cauchy holds

seq is bounded

proof end;