:: BHSP_3 semantic presentation begin deffunc H1( RealUnitarySpace) -> Element of the U1 of \$1 = 0. \$1; definition let X be RealUnitarySpace; let seq be sequence of X; attrseq is Cauchy means :Def1: :: BHSP_3:def 1 for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist ((seq . n),(seq . m)) < r; 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 Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist ((seq . n),(seq . m)) < r ); theorem :: BHSP_3:1 for X being RealUnitarySpace for seq being sequence of X st seq is constant holds seq is Cauchy proof let X be RealUnitarySpace; ::_thesis: for seq being sequence of X st seq is constant holds seq is Cauchy let seq be sequence of X; ::_thesis: ( seq is constant implies seq is Cauchy ) assume A1: seq is constant ; ::_thesis: seq is Cauchy let r be Real; :: according to BHSP_3:def_1 ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist ((seq . n),(seq . m)) < r ) assume A2: r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist ((seq . n),(seq . m)) < r take k = 0 ; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds dist ((seq . n),(seq . m)) < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist ((seq . n),(seq . m)) < r ) assume that n >= k and m >= k ; ::_thesis: dist ((seq . n),(seq . m)) < r dist ((seq . n),(seq . m)) = dist ((seq . n),(seq . n)) by A1, VALUED_0:23 .= 0 by BHSP_1:34 ; hence dist ((seq . n),(seq . m)) < r by A2; ::_thesis: verum end; 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 Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r ) proof let X be RealUnitarySpace; ::_thesis: for seq being sequence of X holds ( seq is Cauchy iff for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r ) let seq be sequence of X; ::_thesis: ( seq is Cauchy iff for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r ) thus ( seq is Cauchy implies for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r ) ::_thesis: ( ( for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r ) implies seq is Cauchy ) proof assume A1: seq is Cauchy ; ::_thesis: for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r then consider l being Element of NAT such that A2: for n, m being Element of NAT st n >= l & m >= l holds dist ((seq . n),(seq . m)) < r by A1, Def1; take k = l; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((seq . n) - (seq . m)).|| < r ) assume ( n >= k & m >= k ) ; ::_thesis: ||.((seq . n) - (seq . m)).|| < r then dist ((seq . n),(seq . m)) < r by A2; hence ||.((seq . n) - (seq . m)).|| < r by BHSP_1:def_5; ::_thesis: verum end; ( ( for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r ) implies seq is Cauchy ) proof assume A3: for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r ; ::_thesis: seq is Cauchy let r be Real; :: according to BHSP_3:def_1 ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist ((seq . n),(seq . m)) < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist ((seq . n),(seq . m)) < r then consider l being Element of NAT such that A4: for n, m being Element of NAT st n >= l & m >= l holds ||.((seq . n) - (seq . m)).|| < r by A3; take k = l; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds dist ((seq . n),(seq . m)) < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist ((seq . n),(seq . m)) < r ) assume ( n >= k & m >= k ) ; ::_thesis: dist ((seq . n),(seq . m)) < r then ||.((seq . n) - (seq . m)).|| < r by A4; hence dist ((seq . n),(seq . m)) < r by BHSP_1:def_5; ::_thesis: verum end; hence ( ( for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r ) implies seq is Cauchy ) ; ::_thesis: verum end; theorem :: BHSP_3:3 for X being RealUnitarySpace for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds seq1 + seq2 is Cauchy proof let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds seq1 + seq2 is Cauchy let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is Cauchy & seq2 is Cauchy implies seq1 + seq2 is Cauchy ) assume that A1: seq1 is Cauchy and A2: seq2 is Cauchy ; ::_thesis: seq1 + seq2 is Cauchy let r be Real; :: according to BHSP_3:def_1 ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) < r then A3: r / 2 > 0 by XREAL_1:215; then consider m1 being Element of NAT such that A4: for n, m being Element of NAT st n >= m1 & m >= m1 holds dist ((seq1 . n),(seq1 . m)) < r / 2 by A1, Def1; consider m2 being Element of NAT such that A5: for n, m being Element of NAT st n >= m2 & m >= m2 holds dist ((seq2 . n),(seq2 . m)) < r / 2 by A2, A3, Def1; take k = m1 + m2; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) < r ) assume A6: ( n >= k & m >= k ) ; ::_thesis: dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) < r k >= m2 by NAT_1:12; then ( n >= m2 & m >= m2 ) by A6, XXREAL_0:2; then A7: dist ((seq2 . n),(seq2 . m)) < r / 2 by A5; dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) = dist (((seq1 . n) + (seq2 . n)),((seq1 + seq2) . m)) by NORMSP_1:def_2 .= dist (((seq1 . n) + (seq2 . n)),((seq1 . m) + (seq2 . m))) by NORMSP_1:def_2 ; then A8: dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) <= (dist ((seq1 . n),(seq1 . m))) + (dist ((seq2 . n),(seq2 . m))) by BHSP_1:40; m1 + m2 >= m1 by NAT_1:12; then ( n >= m1 & m >= m1 ) by A6, XXREAL_0:2; then dist ((seq1 . n),(seq1 . m)) < r / 2 by A4; then (dist ((seq1 . n),(seq1 . m))) + (dist ((seq2 . n),(seq2 . m))) < (r / 2) + (r / 2) by A7, XREAL_1:8; hence dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) < r by A8, XXREAL_0:2; ::_thesis: verum end; theorem :: BHSP_3:4 for X being RealUnitarySpace for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds seq1 - seq2 is Cauchy proof let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds seq1 - seq2 is Cauchy let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is Cauchy & seq2 is Cauchy implies seq1 - seq2 is Cauchy ) assume that A1: seq1 is Cauchy and A2: seq2 is Cauchy ; ::_thesis: seq1 - seq2 is Cauchy let r be Real; :: according to BHSP_3:def_1 ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r then A3: r / 2 > 0 by XREAL_1:215; then consider m1 being Element of NAT such that A4: for n, m being Element of NAT st n >= m1 & m >= m1 holds dist ((seq1 . n),(seq1 . m)) < r / 2 by A1, Def1; consider m2 being Element of NAT such that A5: for n, m being Element of NAT st n >= m2 & m >= m2 holds dist ((seq2 . n),(seq2 . m)) < r / 2 by A2, A3, Def1; take k = m1 + m2; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r ) assume A6: ( n >= k & m >= k ) ; ::_thesis: dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r k >= m2 by NAT_1:12; then ( n >= m2 & m >= m2 ) by A6, XXREAL_0:2; then A7: dist ((seq2 . n),(seq2 . m)) < r / 2 by A5; dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) = dist (((seq1 . n) - (seq2 . n)),((seq1 - seq2) . m)) by NORMSP_1:def_3 .= dist (((seq1 . n) - (seq2 . n)),((seq1 . m) - (seq2 . m))) by NORMSP_1:def_3 ; then A8: dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) <= (dist ((seq1 . n),(seq1 . m))) + (dist ((seq2 . n),(seq2 . m))) by BHSP_1:41; m1 + m2 >= m1 by NAT_1:12; then ( n >= m1 & m >= m1 ) by A6, XXREAL_0:2; then dist ((seq1 . n),(seq1 . m)) < r / 2 by A4; then (dist ((seq1 . n),(seq1 . m))) + (dist ((seq2 . n),(seq2 . m))) < (r / 2) + (r / 2) by A7, XREAL_1:8; hence dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r by A8, XXREAL_0:2; ::_thesis: verum end; theorem Th5: :: BHSP_3:5 for X being RealUnitarySpace for a being Real for seq being sequence of X st seq is Cauchy holds a * seq is Cauchy proof let X be RealUnitarySpace; ::_thesis: for a being Real for seq being sequence of X st seq is Cauchy holds a * seq is Cauchy let a be Real; ::_thesis: for seq being sequence of X st seq is Cauchy holds a * seq is Cauchy let seq be sequence of X; ::_thesis: ( seq is Cauchy implies a * seq is Cauchy ) assume A1: seq is Cauchy ; ::_thesis: a * seq is Cauchy A2: now__::_thesis:_(_a_<>_0_implies_for_r_being_Real_st_r_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_ dist_(((a_*_seq)_._n),((a_*_seq)_._m))_<_r_) A3: 0 / (abs a) = 0 ; assume A4: a <> 0 ; ::_thesis: for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist (((a * seq) . n),((a * seq) . m)) < r then A5: abs a > 0 by COMPLEX1:47; let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist (((a * seq) . n),((a * seq) . m)) < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist (((a * seq) . n),((a * seq) . m)) < r then r / (abs a) > 0 by A5, A3, XREAL_1:74; then consider m1 being Element of NAT such that A6: for n, m being Element of NAT st n >= m1 & m >= m1 holds dist ((seq . n),(seq . m)) < r / (abs a) by A1, Def1; take k = m1; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds dist (((a * seq) . n),((a * seq) . m)) < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist (((a * seq) . n),((a * seq) . m)) < r ) assume ( n >= k & m >= k ) ; ::_thesis: dist (((a * seq) . n),((a * seq) . m)) < r then A7: dist ((seq . n),(seq . m)) < r / (abs a) by A6; A8: abs a <> 0 by A4, COMPLEX1:47; A9: (abs a) * (r / (abs a)) = (abs a) * (((abs a) ") * r) by XCMPLX_0:def_9 .= ((abs a) * ((abs a) ")) * r .= 1 * r by A8, XCMPLX_0:def_7 .= r ; dist ((a * (seq . n)),(a * (seq . m))) = ||.((a * (seq . n)) - (a * (seq . m))).|| by BHSP_1:def_5 .= ||.(a * ((seq . n) - (seq . m))).|| by RLVECT_1:34 .= (abs a) * ||.((seq . n) - (seq . m)).|| by BHSP_1:27 .= (abs a) * (dist ((seq . n),(seq . m))) by BHSP_1:def_5 ; then dist ((a * (seq . n)),(a * (seq . m))) < r by A5, A7, A9, XREAL_1:68; then dist (((a * seq) . n),(a * (seq . m))) < r by NORMSP_1:def_5; hence dist (((a * seq) . n),((a * seq) . m)) < r by NORMSP_1:def_5; ::_thesis: verum end; now__::_thesis:_(_a_=_0_implies_for_r_being_Real_st_r_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_ dist_(((a_*_seq)_._n),((a_*_seq)_._m))_<_r_) assume A10: a = 0 ; ::_thesis: for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist (((a * seq) . n),((a * seq) . m)) < r let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist (((a * seq) . n),((a * seq) . m)) < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist (((a * seq) . n),((a * seq) . m)) < r then consider m1 being Element of NAT such that A11: for n, m being Element of NAT st n >= m1 & m >= m1 holds dist ((seq . n),(seq . m)) < r by A1, Def1; take k = m1; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds dist (((a * seq) . n),((a * seq) . m)) < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist (((a * seq) . n),((a * seq) . m)) < r ) assume ( n >= k & m >= k ) ; ::_thesis: dist (((a * seq) . n),((a * seq) . m)) < r then A12: dist ((seq . n),(seq . m)) < r by A11; dist ((a * (seq . n)),(a * (seq . m))) = dist (H1(X),(0 * (seq . m))) by A10, RLVECT_1:10 .= dist (H1(X),H1(X)) by RLVECT_1:10 .= 0 by BHSP_1:34 ; then dist ((a * (seq . n)),(a * (seq . m))) < r by A12, BHSP_1:37; then dist (((a * seq) . n),(a * (seq . m))) < r by NORMSP_1:def_5; hence dist (((a * seq) . n),((a * seq) . m)) < r by NORMSP_1:def_5; ::_thesis: verum end; hence a * seq is Cauchy by A2, Def1; ::_thesis: verum end; theorem :: BHSP_3:6 for X being RealUnitarySpace for seq being sequence of X st seq is Cauchy holds - seq is Cauchy proof let X be RealUnitarySpace; ::_thesis: for seq being sequence of X st seq is Cauchy holds - seq is Cauchy let seq be sequence of X; ::_thesis: ( seq is Cauchy implies - seq is Cauchy ) assume seq is Cauchy ; ::_thesis: - seq is Cauchy then (- 1) * seq is Cauchy by Th5; hence - seq is Cauchy by BHSP_1:55; ::_thesis: verum end; theorem Th7: :: BHSP_3:7 for X being RealUnitarySpace for x being Point of X for seq being sequence of X st seq is Cauchy holds seq + x is Cauchy proof let X be RealUnitarySpace; ::_thesis: for x being Point of X for seq being sequence of X st seq is Cauchy holds seq + x is Cauchy let x be Point of X; ::_thesis: for seq being sequence of X st seq is Cauchy holds seq + x is Cauchy let seq be sequence of X; ::_thesis: ( seq is Cauchy implies seq + x is Cauchy ) assume A1: seq is Cauchy ; ::_thesis: seq + x is Cauchy let r be Real; :: according to BHSP_3:def_1 ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist (((seq + x) . n),((seq + x) . m)) < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist (((seq + x) . n),((seq + x) . m)) < r then consider m1 being Element of NAT such that A2: for n, m being Element of NAT st n >= m1 & m >= m1 holds dist ((seq . n),(seq . m)) < r by A1, Def1; take k = m1; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds dist (((seq + x) . n),((seq + x) . m)) < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist (((seq + x) . n),((seq + x) . m)) < r ) dist (((seq . n) + x),((seq . m) + x)) <= (dist ((seq . n),(seq . m))) + (dist (x,x)) by BHSP_1:40; then A3: dist (((seq . n) + x),((seq . m) + x)) <= (dist ((seq . n),(seq . m))) + 0 by BHSP_1:34; assume ( n >= k & m >= k ) ; ::_thesis: dist (((seq + x) . n),((seq + x) . m)) < r then dist ((seq . n),(seq . m)) < r by A2; then dist (((seq . n) + x),((seq . m) + x)) < r by A3, XXREAL_0:2; then dist (((seq + x) . n),((seq . m) + x)) < r by BHSP_1:def_6; hence dist (((seq + x) . n),((seq + x) . m)) < r by BHSP_1:def_6; ::_thesis: verum end; theorem :: BHSP_3:8 for X being RealUnitarySpace for x being Point of X for seq being sequence of X st seq is Cauchy holds seq - x is Cauchy proof let X be RealUnitarySpace; ::_thesis: for x being Point of X for seq being sequence of X st seq is Cauchy holds seq - x is Cauchy let x be Point of X; ::_thesis: for seq being sequence of X st seq is Cauchy holds seq - x is Cauchy let seq be sequence of X; ::_thesis: ( seq is Cauchy implies seq - x is Cauchy ) assume seq is Cauchy ; ::_thesis: seq - x is Cauchy then seq + (- x) is Cauchy by Th7; hence seq - x is Cauchy by BHSP_1:56; ::_thesis: verum end; theorem :: BHSP_3:9 for X being RealUnitarySpace for seq being sequence of X st seq is convergent holds seq is Cauchy proof let X be RealUnitarySpace; ::_thesis: for seq being sequence of X st seq is convergent holds seq is Cauchy let seq be sequence of X; ::_thesis: ( seq is convergent implies seq is Cauchy ) assume seq is convergent ; ::_thesis: seq is Cauchy then consider h being Point of X such that A1: for r being Real st r > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds dist ((seq . n),h) < r by BHSP_2:def_1; let r be Real; :: according to BHSP_3:def_1 ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist ((seq . n),(seq . m)) < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist ((seq . n),(seq . m)) < r then consider m1 being Element of NAT such that A2: for n being Element of NAT st n >= m1 holds dist ((seq . n),h) < r / 2 by A1, XREAL_1:215; take k = m1; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds dist ((seq . n),(seq . m)) < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist ((seq . n),(seq . m)) < r ) assume ( n >= k & m >= k ) ; ::_thesis: dist ((seq . n),(seq . m)) < r then ( dist ((seq . n),h) < r / 2 & dist ((seq . m),h) < r / 2 ) by A2; then ( dist ((seq . n),(seq . m)) <= (dist ((seq . n),h)) + (dist (h,(seq . m))) & (dist ((seq . n),h)) + (dist (h,(seq . m))) < (r / 2) + (r / 2) ) by BHSP_1:35, XREAL_1:8; hence dist ((seq . n),(seq . m)) < r by XXREAL_0:2; ::_thesis: verum end; definition let X be RealUnitarySpace; let seq1, seq2 be sequence of X; predseq1 is_compared_to seq2 means :Def2: :: BHSP_3:def 2 for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq1 . n),(seq2 . n)) < r; end; :: deftheorem Def2 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 Element of NAT st for n being Element of NAT st n >= m holds dist ((seq1 . n),(seq2 . n)) < r ); theorem Th10: :: BHSP_3:10 for X being RealUnitarySpace for seq being sequence of X holds seq is_compared_to seq proof let X be RealUnitarySpace; ::_thesis: for seq being sequence of X holds seq is_compared_to seq let seq be sequence of X; ::_thesis: seq is_compared_to seq let r be Real; :: according to BHSP_3:def_2 ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq . n),(seq . n)) < r ) assume A1: r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq . n),(seq . n)) < r take m = 0 ; ::_thesis: for n being Element of NAT st n >= m holds dist ((seq . n),(seq . n)) < r let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq . n),(seq . n)) < r ) assume n >= m ; ::_thesis: dist ((seq . n),(seq . n)) < r thus dist ((seq . n),(seq . n)) < r by A1, BHSP_1:34; ::_thesis: verum end; theorem Th11: :: BHSP_3:11 for X being RealUnitarySpace for seq1, seq2 being sequence of X st seq1 is_compared_to seq2 holds seq2 is_compared_to seq1 proof let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is_compared_to seq2 holds seq2 is_compared_to seq1 let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is_compared_to seq2 implies seq2 is_compared_to seq1 ) assume A1: seq1 is_compared_to seq2 ; ::_thesis: seq2 is_compared_to seq1 let r be Real; :: according to BHSP_3:def_2 ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq2 . n),(seq1 . n)) < r ) assume r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq2 . n),(seq1 . n)) < r then consider k being Element of NAT such that A2: for n being Element of NAT st n >= k holds dist ((seq1 . n),(seq2 . n)) < r by A1, Def2; take m = k; ::_thesis: for n being Element of NAT st n >= m holds dist ((seq2 . n),(seq1 . n)) < r let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq2 . n),(seq1 . n)) < r ) assume n >= m ; ::_thesis: dist ((seq2 . n),(seq1 . n)) < r hence dist ((seq2 . n),(seq1 . n)) < r by A2; ::_thesis: verum end; definition let X be RealUnitarySpace; let seq1, seq2 be sequence of X; :: original: is_compared_to redefine predseq1 is_compared_to seq2; reflexivity for seq1 being sequence of X holds (X,b1,b1) by Th10; symmetry for seq1, seq2 being sequence of X st (X,b1,b2) holds (X,b2,b1) by Th11; end; 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 proof let X be RealUnitarySpace; ::_thesis: 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 let seq1, seq2, seq3 be sequence of X; ::_thesis: ( seq1 is_compared_to seq2 & seq2 is_compared_to seq3 implies seq1 is_compared_to seq3 ) assume that A1: seq1 is_compared_to seq2 and A2: seq2 is_compared_to seq3 ; ::_thesis: seq1 is_compared_to seq3 let r be Real; :: according to BHSP_3:def_2 ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq1 . n),(seq3 . n)) < r ) assume r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq1 . n),(seq3 . n)) < r then A3: r / 2 > 0 by XREAL_1:215; then consider m1 being Element of NAT such that A4: for n being Element of NAT st n >= m1 holds dist ((seq1 . n),(seq2 . n)) < r / 2 by A1, Def2; consider m2 being Element of NAT such that A5: for n being Element of NAT st n >= m2 holds dist ((seq2 . n),(seq3 . n)) < r / 2 by A2, A3, Def2; take m = m1 + m2; ::_thesis: for n being Element of NAT st n >= m holds dist ((seq1 . n),(seq3 . n)) < r let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq1 . n),(seq3 . n)) < r ) assume A6: n >= m ; ::_thesis: dist ((seq1 . n),(seq3 . n)) < r m >= m2 by NAT_1:12; then n >= m2 by A6, XXREAL_0:2; then A7: dist ((seq2 . n),(seq3 . n)) < r / 2 by A5; A8: dist ((seq1 . n),(seq3 . n)) <= (dist ((seq1 . n),(seq2 . n))) + (dist ((seq2 . n),(seq3 . n))) by BHSP_1:35; m1 + m2 >= m1 by NAT_1:12; then n >= m1 by A6, XXREAL_0:2; then dist ((seq1 . n),(seq2 . n)) < r / 2 by A4; then (dist ((seq1 . n),(seq2 . n))) + (dist ((seq2 . n),(seq3 . n))) < (r / 2) + (r / 2) by A7, XREAL_1:8; hence dist ((seq1 . n),(seq3 . n)) < r by A8, XXREAL_0:2; ::_thesis: verum 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 Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r ) proof let X be RealUnitarySpace; ::_thesis: 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 Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r ) let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is_compared_to seq2 iff for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r ) thus ( seq1 is_compared_to seq2 implies for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r ) ::_thesis: ( ( for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r ) implies seq1 is_compared_to seq2 ) proof assume A1: seq1 is_compared_to seq2 ; ::_thesis: for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r ) assume r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r then consider m1 being Element of NAT such that A2: for n being Element of NAT st n >= m1 holds dist ((seq1 . n),(seq2 . n)) < r by A1, Def2; take m = m1; ::_thesis: for n being Element of NAT st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((seq1 . n) - (seq2 . n)).|| < r ) assume n >= m ; ::_thesis: ||.((seq1 . n) - (seq2 . n)).|| < r then dist ((seq1 . n),(seq2 . n)) < r by A2; hence ||.((seq1 . n) - (seq2 . n)).|| < r by BHSP_1:def_5; ::_thesis: verum end; ( ( for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r ) implies seq1 is_compared_to seq2 ) proof assume A3: for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r ; ::_thesis: seq1 is_compared_to seq2 let r be Real; :: according to BHSP_3:def_2 ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq1 . n),(seq2 . n)) < r ) assume r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq1 . n),(seq2 . n)) < r then consider m1 being Element of NAT such that A4: for n being Element of NAT st n >= m1 holds ||.((seq1 . n) - (seq2 . n)).|| < r by A3; take m = m1; ::_thesis: for n being Element of NAT st n >= m holds dist ((seq1 . n),(seq2 . n)) < r let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq1 . n),(seq2 . n)) < r ) assume n >= m ; ::_thesis: dist ((seq1 . n),(seq2 . n)) < r then ||.((seq1 . n) - (seq2 . n)).|| < r by A4; hence dist ((seq1 . n),(seq2 . n)) < r by BHSP_1:def_5; ::_thesis: verum end; hence ( ( for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - (seq2 . n)).|| < r ) implies seq1 is_compared_to seq2 ) ; ::_thesis: verum end; theorem :: BHSP_3:14 for X being RealUnitarySpace for seq1, seq2 being sequence of X st ex k being Element of NAT st for n being Element of NAT st n >= k holds seq1 . n = seq2 . n holds seq1 is_compared_to seq2 proof let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st ex k being Element of NAT st for n being Element of NAT st n >= k holds seq1 . n = seq2 . n holds seq1 is_compared_to seq2 let seq1, seq2 be sequence of X; ::_thesis: ( ex k being Element of NAT st for n being Element of NAT st n >= k holds seq1 . n = seq2 . n implies seq1 is_compared_to seq2 ) assume ex k being Element of NAT st for n being Element of NAT st n >= k holds seq1 . n = seq2 . n ; ::_thesis: seq1 is_compared_to seq2 then consider m being Element of NAT such that A1: for n being Element of NAT st n >= m holds seq1 . n = seq2 . n ; let r be Real; :: according to BHSP_3:def_2 ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq1 . n),(seq2 . n)) < r ) assume A2: r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq1 . n),(seq2 . n)) < r take k = m; ::_thesis: for n being Element of NAT st n >= k holds dist ((seq1 . n),(seq2 . n)) < r let n be Element of NAT ; ::_thesis: ( n >= k implies dist ((seq1 . n),(seq2 . n)) < r ) assume n >= k ; ::_thesis: dist ((seq1 . n),(seq2 . n)) < r then dist ((seq1 . n),(seq2 . n)) = dist ((seq1 . n),(seq1 . n)) by A1 .= 0 by BHSP_1:34 ; hence dist ((seq1 . n),(seq2 . n)) < r by A2; ::_thesis: verum 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 proof let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is Cauchy & seq1 is_compared_to seq2 holds seq2 is Cauchy let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is Cauchy & seq1 is_compared_to seq2 implies seq2 is Cauchy ) assume that A1: seq1 is Cauchy and A2: seq1 is_compared_to seq2 ; ::_thesis: seq2 is Cauchy let r be Real; :: according to BHSP_3:def_1 ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist ((seq2 . n),(seq2 . m)) < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist ((seq2 . n),(seq2 . m)) < r then A3: r / 3 > 0 by XREAL_1:222; then consider m1 being Element of NAT such that A4: for n, m being Element of NAT st n >= m1 & m >= m1 holds dist ((seq1 . n),(seq1 . m)) < r / 3 by A1, Def1; consider m2 being Element of NAT such that A5: for n being Element of NAT st n >= m2 holds dist ((seq1 . n),(seq2 . n)) < r / 3 by A2, A3, Def2; take k = m1 + m2; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds dist ((seq2 . n),(seq2 . m)) < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist ((seq2 . n),(seq2 . m)) < r ) assume that A6: n >= k and A7: m >= k ; ::_thesis: dist ((seq2 . n),(seq2 . m)) < r m1 + m2 >= m1 by NAT_1:12; then ( n >= m1 & m >= m1 ) by A6, A7, XXREAL_0:2; then A8: dist ((seq1 . n),(seq1 . m)) < r / 3 by A4; A9: dist ((seq2 . n),(seq1 . m)) <= (dist ((seq2 . n),(seq1 . n))) + (dist ((seq1 . n),(seq1 . m))) by BHSP_1:35; A10: k >= m2 by NAT_1:12; then n >= m2 by A6, XXREAL_0:2; then dist ((seq1 . n),(seq2 . n)) < r / 3 by A5; then (dist ((seq2 . n),(seq1 . n))) + (dist ((seq1 . n),(seq1 . m))) < (r / 3) + (r / 3) by A8, XREAL_1:8; then A11: dist ((seq2 . n),(seq1 . m)) < (r / 3) + (r / 3) by A9, XXREAL_0:2; A12: dist ((seq2 . n),(seq2 . m)) <= (dist ((seq2 . n),(seq1 . m))) + (dist ((seq1 . m),(seq2 . m))) by BHSP_1:35; m >= m2 by A7, A10, XXREAL_0:2; then dist ((seq1 . m),(seq2 . m)) < r / 3 by A5; then (dist ((seq2 . n),(seq1 . m))) + (dist ((seq1 . m),(seq2 . m))) < ((r / 3) + (r / 3)) + (r / 3) by A11, XREAL_1:8; hence dist ((seq2 . n),(seq2 . m)) < r by A12, XXREAL_0:2; ::_thesis: verum 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 proof let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & seq1 is_compared_to seq2 holds seq2 is convergent let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & seq1 is_compared_to seq2 implies seq2 is convergent ) assume that A1: seq1 is convergent and A2: seq1 is_compared_to seq2 ; ::_thesis: seq2 is convergent now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_m_holds_ dist_((seq2_._n),(lim_seq1))_<_r let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq2 . n),(lim seq1)) < r ) assume r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq2 . n),(lim seq1)) < r then A3: r / 2 > 0 by XREAL_1:215; then consider m1 being Element of NAT such that A4: for n being Element of NAT st n >= m1 holds dist ((seq1 . n),(lim seq1)) < r / 2 by A1, BHSP_2:def_2; consider m2 being Element of NAT such that A5: for n being Element of NAT st n >= m2 holds dist ((seq1 . n),(seq2 . n)) < r / 2 by A2, A3, Def2; take m = m1 + m2; ::_thesis: for n being Element of NAT st n >= m holds dist ((seq2 . n),(lim seq1)) < r let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq2 . n),(lim seq1)) < r ) assume A6: n >= m ; ::_thesis: dist ((seq2 . n),(lim seq1)) < r m >= m2 by NAT_1:12; then n >= m2 by A6, XXREAL_0:2; then A7: dist ((seq1 . n),(seq2 . n)) < r / 2 by A5; A8: dist ((seq2 . n),(lim seq1)) <= (dist ((seq2 . n),(seq1 . n))) + (dist ((seq1 . n),(lim seq1))) by BHSP_1:35; m1 + m2 >= m1 by NAT_1:12; then n >= m1 by A6, XXREAL_0:2; then dist ((seq1 . n),(lim seq1)) < r / 2 by A4; then (dist ((seq2 . n),(seq1 . n))) + (dist ((seq1 . n),(lim seq1))) < (r / 2) + (r / 2) by A7, XREAL_1:8; hence dist ((seq2 . n),(lim seq1)) < r by A8, XXREAL_0:2; ::_thesis: verum end; hence seq2 is convergent by BHSP_2:def_1; ::_thesis: verum 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 ) proof let X be RealUnitarySpace; ::_thesis: 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 ) let g be Point of X; ::_thesis: 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 ) let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 implies ( seq2 is convergent & lim seq2 = g ) ) assume that A1: ( seq1 is convergent & lim seq1 = g ) and A2: seq1 is_compared_to seq2 ; ::_thesis: ( seq2 is convergent & lim seq2 = g ) A3: now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_m_holds_ dist_((seq2_._n),g)_<_r let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq2 . n),g) < r ) assume r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq2 . n),g) < r then A4: r / 2 > 0 by XREAL_1:215; then consider m1 being Element of NAT such that A5: for n being Element of NAT st n >= m1 holds dist ((seq1 . n),g) < r / 2 by A1, BHSP_2:def_2; consider m2 being Element of NAT such that A6: for n being Element of NAT st n >= m2 holds dist ((seq1 . n),(seq2 . n)) < r / 2 by A2, A4, Def2; take m = m1 + m2; ::_thesis: for n being Element of NAT st n >= m holds dist ((seq2 . n),g) < r let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq2 . n),g) < r ) assume A7: n >= m ; ::_thesis: dist ((seq2 . n),g) < r m >= m2 by NAT_1:12; then n >= m2 by A7, XXREAL_0:2; then A8: dist ((seq1 . n),(seq2 . n)) < r / 2 by A6; A9: dist ((seq2 . n),g) <= (dist ((seq2 . n),(seq1 . n))) + (dist ((seq1 . n),g)) by BHSP_1:35; m1 + m2 >= m1 by NAT_1:12; then n >= m1 by A7, XXREAL_0:2; then dist ((seq1 . n),g) < r / 2 by A5; then (dist ((seq2 . n),(seq1 . n))) + (dist ((seq1 . n),g)) < (r / 2) + (r / 2) by A8, XREAL_1:8; hence dist ((seq2 . n),g) < r by A9, XXREAL_0:2; ::_thesis: verum end; then seq2 is convergent by BHSP_2:def_1; hence ( seq2 is convergent & lim seq2 = g ) by A3, BHSP_2:def_2; ::_thesis: verum end; definition let X be RealUnitarySpace; let seq be sequence of X; attrseq is bounded means :Def3: :: BHSP_3:def 3 ex M being Real st ( M > 0 & ( for n being Element of NAT holds ||.(seq . n).|| <= M ) ); 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 Element of NAT holds ||.(seq . n).|| <= M ) ) ); theorem Th18: :: BHSP_3:18 for X being RealUnitarySpace for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds seq1 + seq2 is bounded proof let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds seq1 + seq2 is bounded let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is bounded & seq2 is bounded implies seq1 + seq2 is bounded ) assume that A1: seq1 is bounded and A2: seq2 is bounded ; ::_thesis: seq1 + seq2 is bounded consider M2 being Real such that A3: M2 > 0 and A4: for n being Element of NAT holds ||.(seq2 . n).|| <= M2 by A2, Def3; consider M1 being Real such that A5: M1 > 0 and A6: for n being Element of NAT holds ||.(seq1 . n).|| <= M1 by A1, Def3; now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((seq1_+_seq2)_._n).||_<=_M1_+_M2 let n be Element of NAT ; ::_thesis: ||.((seq1 + seq2) . n).|| <= M1 + M2 ||.((seq1 + seq2) . n).|| = ||.((seq1 . n) + (seq2 . n)).|| by NORMSP_1:def_2; then A7: ||.((seq1 + seq2) . n).|| <= ||.(seq1 . n).|| + ||.(seq2 . n).|| by BHSP_1:30; ( ||.(seq1 . n).|| <= M1 & ||.(seq2 . n).|| <= M2 ) by A6, A4; then ||.(seq1 . n).|| + ||.(seq2 . n).|| <= M1 + M2 by XREAL_1:7; hence ||.((seq1 + seq2) . n).|| <= M1 + M2 by A7, XXREAL_0:2; ::_thesis: verum end; hence seq1 + seq2 is bounded by A5, A3, Def3; ::_thesis: verum end; theorem Th19: :: BHSP_3:19 for X being RealUnitarySpace for seq being sequence of X st seq is bounded holds - seq is bounded proof let X be RealUnitarySpace; ::_thesis: for seq being sequence of X st seq is bounded holds - seq is bounded let seq be sequence of X; ::_thesis: ( seq is bounded implies - seq is bounded ) assume seq is bounded ; ::_thesis: - seq is bounded then consider M being Real such that A1: M > 0 and A2: for n being Element of NAT holds ||.(seq . n).|| <= M by Def3; now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((-_seq)_._n).||_<=_M let n be Element of NAT ; ::_thesis: ||.((- seq) . n).|| <= M ||.((- seq) . n).|| = ||.(- (seq . n)).|| by BHSP_1:44 .= ||.(seq . n).|| by BHSP_1:31 ; hence ||.((- seq) . n).|| <= M by A2; ::_thesis: verum end; hence - seq is bounded by A1, Def3; ::_thesis: verum end; theorem :: BHSP_3:20 for X being RealUnitarySpace for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds seq1 - seq2 is bounded proof let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds seq1 - seq2 is bounded let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is bounded & seq2 is bounded implies seq1 - seq2 is bounded ) assume that A1: seq1 is bounded and A2: seq2 is bounded ; ::_thesis: seq1 - seq2 is bounded A3: seq1 - seq2 = seq1 + (- seq2) by BHSP_1:49; - seq2 is bounded by A2, Th19; hence seq1 - seq2 is bounded by A1, A3, Th18; ::_thesis: verum end; theorem :: BHSP_3:21 for X being RealUnitarySpace for a being Real for seq being sequence of X st seq is bounded holds a * seq is bounded proof let X be RealUnitarySpace; ::_thesis: for a being Real for seq being sequence of X st seq is bounded holds a * seq is bounded let a be Real; ::_thesis: for seq being sequence of X st seq is bounded holds a * seq is bounded let seq be sequence of X; ::_thesis: ( seq is bounded implies a * seq is bounded ) assume seq is bounded ; ::_thesis: a * seq is bounded then consider M being Real such that A1: M > 0 and A2: for n being Element of NAT holds ||.(seq . n).|| <= M by Def3; A3: ( a <> 0 implies a * seq is bounded ) proof A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((a_*_seq)_._n).||_<=_(abs_a)_*_M let n be Element of NAT ; ::_thesis: ||.((a * seq) . n).|| <= (abs a) * M A5: abs a >= 0 by COMPLEX1:46; ||.((a * seq) . n).|| = ||.(a * (seq . n)).|| by NORMSP_1:def_5 .= (abs a) * ||.(seq . n).|| by BHSP_1:27 ; hence ||.((a * seq) . n).|| <= (abs a) * M by A2, A5, XREAL_1:64; ::_thesis: verum end; assume a <> 0 ; ::_thesis: a * seq is bounded then abs a > 0 by COMPLEX1:47; then (abs a) * M > 0 by A1, XREAL_1:129; hence a * seq is bounded by A4, Def3; ::_thesis: verum end; ( a = 0 implies a * seq is bounded ) proof assume A6: a = 0 ; ::_thesis: a * seq is bounded now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((a_*_seq)_._n).||_<=_M let n be Element of NAT ; ::_thesis: ||.((a * seq) . n).|| <= M ||.((a * seq) . n).|| = ||.(0 * (seq . n)).|| by A6, NORMSP_1:def_5 .= ||.H1(X).|| by RLVECT_1:10 .= 0 by BHSP_1:26 ; hence ||.((a * seq) . n).|| <= M by A1; ::_thesis: verum end; hence a * seq is bounded by A1, Def3; ::_thesis: verum end; hence a * seq is bounded by A3; ::_thesis: verum end; theorem :: BHSP_3:22 for X being RealUnitarySpace for seq being sequence of X st seq is constant holds seq is bounded proof let X be RealUnitarySpace; ::_thesis: for seq being sequence of X st seq is constant holds seq is bounded let seq be sequence of X; ::_thesis: ( seq is constant implies seq is bounded ) assume seq is constant ; ::_thesis: seq is bounded then consider x being Point of X such that A1: for n being Nat holds seq . n = x by VALUED_0:def_18; A2: ( x = H1(X) implies seq is bounded ) proof consider M being real number such that A3: M > 0 by XREAL_1:1; reconsider M = M as Real by XREAL_0:def_1; assume A4: x = H1(X) ; ::_thesis: seq is bounded now__::_thesis:_for_n_being_Element_of_NAT_holds_||.(seq_._n).||_<=_M let n be Element of NAT ; ::_thesis: ||.(seq . n).|| <= M seq . n = H1(X) by A1, A4; hence ||.(seq . n).|| <= M by A3, BHSP_1:26; ::_thesis: verum end; hence seq is bounded by A3, Def3; ::_thesis: verum end; ( x <> H1(X) implies seq is bounded ) proof assume x <> H1(X) ; ::_thesis: seq is bounded consider M being real number such that A5: ||.x.|| < M by XREAL_1:1; reconsider M = M as Real by XREAL_0:def_1; ( ||.x.|| >= 0 & ( for n being Element of NAT holds ||.(seq . n).|| <= M ) ) by A1, A5, BHSP_1:28; hence seq is bounded by A5, Def3; ::_thesis: verum end; hence seq is bounded by A2; ::_thesis: verum end; theorem Th23: :: BHSP_3:23 for X being RealUnitarySpace for seq being sequence of X for m being Element of NAT ex M being Real st ( M > 0 & ( for n being Element of NAT st n <= m holds ||.(seq . n).|| < M ) ) proof let X be RealUnitarySpace; ::_thesis: for seq being sequence of X for m being Element of NAT ex M being Real st ( M > 0 & ( for n being Element of NAT st n <= m holds ||.(seq . n).|| < M ) ) let seq be sequence of X; ::_thesis: for m being Element of NAT ex M being Real st ( M > 0 & ( for n being Element of NAT st n <= m holds ||.(seq . n).|| < M ) ) defpred S1[ Element of NAT ] means ex M being Real st ( M > 0 & ( for n being Element of NAT st n <= \$1 holds ||.(seq . n).|| < M ) ); A1: for m being Element of NAT st S1[m] holds S1[m + 1] proof let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) given M1 being Real such that A2: M1 > 0 and A3: for n being Element of NAT st n <= m holds ||.(seq . n).|| < M1 ; ::_thesis: S1[m + 1] A4: now__::_thesis:_(_||.(seq_._(m_+_1)).||_>=_M1_implies_ex_M_being_Element_of_REAL_st_ (_M_>_0_&_(_for_n_being_Element_of_NAT_st_n_<=_m_+_1_holds_ ||.(seq_._n).||_<_M_)_)_) assume A5: ||.(seq . (m + 1)).|| >= M1 ; ::_thesis: ex M being Element of REAL st ( M > 0 & ( for n being Element of NAT st n <= m + 1 holds ||.(seq . n).|| < M ) ) take M = ||.(seq . (m + 1)).|| + 1; ::_thesis: ( M > 0 & ( for n being Element of NAT st n <= m + 1 holds ||.(seq . n).|| < M ) ) M > 0 + 0 by BHSP_1:28, XREAL_1:8; hence M > 0 ; ::_thesis: for n being Element of NAT st n <= m + 1 holds ||.(seq . n).|| < M let n be Element of NAT ; ::_thesis: ( n <= m + 1 implies ||.(seq . n).|| < M ) assume A6: n <= m + 1 ; ::_thesis: ||.(seq . n).|| < M A7: now__::_thesis:_(_m_>=_n_implies_||.(seq_._n).||_<_M_) assume m >= n ; ::_thesis: ||.(seq . n).|| < M then ||.(seq . n).|| < M1 by A3; then ||.(seq . n).|| < ||.(seq . (m + 1)).|| by A5, XXREAL_0:2; then ||.(seq . n).|| + 0 < M by XREAL_1:8; hence ||.(seq . n).|| < M ; ::_thesis: verum end; now__::_thesis:_(_n_=_m_+_1_implies_||.(seq_._n).||_<_M_) assume n = m + 1 ; ::_thesis: ||.(seq . n).|| < M then ||.(seq . n).|| + 0 < M by XREAL_1:8; hence ||.(seq . n).|| < M ; ::_thesis: verum end; hence ||.(seq . n).|| < M by A6, A7, NAT_1:8; ::_thesis: verum end; now__::_thesis:_(_||.(seq_._(m_+_1)).||_<=_M1_implies_ex_M_being_Element_of_REAL_st_ (_M_>_0_&_(_for_n_being_Element_of_NAT_st_n_<=_m_+_1_holds_ ||.(seq_._n).||_<_M_)_)_) assume A8: ||.(seq . (m + 1)).|| <= M1 ; ::_thesis: ex M being Element of REAL st ( M > 0 & ( for n being Element of NAT st n <= m + 1 holds ||.(seq . n).|| < M ) ) take M = M1 + 1; ::_thesis: ( M > 0 & ( for n being Element of NAT st n <= m + 1 holds ||.(seq . n).|| < M ) ) thus M > 0 by A2; ::_thesis: for n being Element of NAT st n <= m + 1 holds ||.(seq . n).|| < M let n be Element of NAT ; ::_thesis: ( n <= m + 1 implies ||.(seq . n).|| < M ) assume A9: n <= m + 1 ; ::_thesis: ||.(seq . n).|| < M A10: now__::_thesis:_(_m_>=_n_implies_||.(seq_._n).||_<_M_) assume m >= n ; ::_thesis: ||.(seq . n).|| < M then A11: ||.(seq . n).|| < M1 by A3; M > M1 + 0 by XREAL_1:8; hence ||.(seq . n).|| < M by A11, XXREAL_0:2; ::_thesis: verum end; now__::_thesis:_(_n_=_m_+_1_implies_||.(seq_._n).||_<_M_) A12: M > M1 + 0 by XREAL_1:8; assume n = m + 1 ; ::_thesis: ||.(seq . n).|| < M hence ||.(seq . n).|| < M by A8, A12, XXREAL_0:2; ::_thesis: verum end; hence ||.(seq . n).|| < M by A9, A10, NAT_1:8; ::_thesis: verum end; hence S1[m + 1] by A4; ::_thesis: verum end; A13: S1[ 0 ] proof take M = ||.(seq . 0).|| + 1; ::_thesis: ( M > 0 & ( for n being Element of NAT st n <= 0 holds ||.(seq . n).|| < M ) ) ||.(seq . 0).|| + 1 > 0 + 0 by BHSP_1:28, XREAL_1:8; hence M > 0 ; ::_thesis: for n being Element of NAT st n <= 0 holds ||.(seq . n).|| < M let n be Element of NAT ; ::_thesis: ( n <= 0 implies ||.(seq . n).|| < M ) assume n <= 0 ; ::_thesis: ||.(seq . n).|| < M then n = 0 ; then ||.(seq . n).|| + 0 < M by XREAL_1:8; hence ||.(seq . n).|| < M ; ::_thesis: verum end; thus for m being Element of NAT holds S1[m] from NAT_1:sch_1(A13, A1); ::_thesis: verum end; theorem Th24: :: BHSP_3:24 for X being RealUnitarySpace for seq being sequence of X st seq is convergent holds seq is bounded proof let X be RealUnitarySpace; ::_thesis: for seq being sequence of X st seq is convergent holds seq is bounded let seq be sequence of X; ::_thesis: ( seq is convergent implies seq is bounded ) assume seq is convergent ; ::_thesis: seq is bounded then consider g being Point of X such that A1: for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq . n) - g).|| < r by BHSP_2:9; consider m1 being Element of NAT such that A2: for n being Element of NAT st n >= m1 holds ||.((seq . n) - g).|| < 1 by A1; A3: now__::_thesis:_ex_p_being_Element_of_REAL_st_ (_p_>_0_&_(_for_n_being_Element_of_NAT_st_n_>=_m1_holds_ ||.(seq_._n).||_<_p_)_) take p = ||.g.|| + 1; ::_thesis: ( p > 0 & ( for n being Element of NAT st n >= m1 holds ||.(seq . n).|| < p ) ) 0 + 0 < p by BHSP_1:28, XREAL_1:8; hence p > 0 ; ::_thesis: for n being Element of NAT st n >= m1 holds ||.(seq . n).|| < p let n be Element of NAT ; ::_thesis: ( n >= m1 implies ||.(seq . n).|| < p ) assume n >= m1 ; ::_thesis: ||.(seq . n).|| < p then A4: ||.((seq . n) - g).|| < 1 by A2; ||.(seq . n).|| - ||.g.|| <= ||.((seq . n) - g).|| by BHSP_1:32; then ||.(seq . n).|| - ||.g.|| < 1 by A4, XXREAL_0:2; hence ||.(seq . n).|| < p by XREAL_1:19; ::_thesis: verum end; now__::_thesis:_ex_M_being_Element_of_REAL_st_ (_M_>_0_&_(_for_n_being_Element_of_NAT_holds_||.(seq_._n).||_<=_M_)_) consider M2 being Real such that A5: M2 > 0 and A6: for n being Element of NAT st n <= m1 holds ||.(seq . n).|| < M2 by Th23; consider M1 being Real such that A7: M1 > 0 and A8: for n being Element of NAT st n >= m1 holds ||.(seq . n).|| < M1 by A3; take M = M1 + M2; ::_thesis: ( M > 0 & ( for n being Element of NAT holds ||.(seq . n).|| <= M ) ) thus M > 0 by A7, A5; ::_thesis: for n being Element of NAT holds ||.(seq . n).|| <= M let n be Element of NAT ; ::_thesis: ||.(seq . n).|| <= M A9: M > 0 + M2 by A7, XREAL_1:8; A10: now__::_thesis:_(_n_<=_m1_implies_||.(seq_._n).||_<=_M_) assume n <= m1 ; ::_thesis: ||.(seq . n).|| <= M then ||.(seq . n).|| < M2 by A6; hence ||.(seq . n).|| <= M by A9, XXREAL_0:2; ::_thesis: verum end; A11: M > M1 + 0 by A5, XREAL_1:8; now__::_thesis:_(_n_>=_m1_implies_||.(seq_._n).||_<=_M_) assume n >= m1 ; ::_thesis: ||.(seq . n).|| <= M then ||.(seq . n).|| < M1 by A8; hence ||.(seq . n).|| <= M by A11, XXREAL_0:2; ::_thesis: verum end; hence ||.(seq . n).|| <= M by A10; ::_thesis: verum end; hence seq is bounded by Def3; ::_thesis: verum end; 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 proof let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is bounded & seq1 is_compared_to seq2 holds seq2 is bounded let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is bounded & seq1 is_compared_to seq2 implies seq2 is bounded ) assume that A1: seq1 is bounded and A2: seq1 is_compared_to seq2 ; ::_thesis: seq2 is bounded consider m1 being Element of NAT such that A3: for n being Element of NAT st n >= m1 holds dist ((seq1 . n),(seq2 . n)) < 1 by A2, Def2; consider p being Real such that A4: p > 0 and A5: for n being Element of NAT holds ||.(seq1 . n).|| <= p by A1, Def3; A6: ex M being Real st ( M > 0 & ( for n being Element of NAT st n >= m1 holds ||.(seq2 . n).|| < M ) ) proof take M = p + 1; ::_thesis: ( M > 0 & ( for n being Element of NAT st n >= m1 holds ||.(seq2 . n).|| < M ) ) now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m1_holds_ ||.(seq2_._n).||_<_M let n be Element of NAT ; ::_thesis: ( n >= m1 implies ||.(seq2 . n).|| < M ) assume n >= m1 ; ::_thesis: ||.(seq2 . n).|| < M then dist ((seq1 . n),(seq2 . n)) < 1 by A3; then A7: ||.((seq2 . n) - (seq1 . n)).|| < 1 by BHSP_1:def_5; ||.(seq2 . n).|| - ||.(seq1 . n).|| <= ||.((seq2 . n) - (seq1 . n)).|| by BHSP_1:32; then ||.(seq2 . n).|| - ||.(seq1 . n).|| < 1 by A7, XXREAL_0:2; then A8: ||.(seq2 . n).|| < ||.(seq1 . n).|| + 1 by XREAL_1:19; ||.(seq1 . n).|| <= p by A5; then ||.(seq1 . n).|| + 1 <= p + 1 by XREAL_1:6; hence ||.(seq2 . n).|| < M by A8, XXREAL_0:2; ::_thesis: verum end; hence ( M > 0 & ( for n being Element of NAT st n >= m1 holds ||.(seq2 . n).|| < M ) ) by A4; ::_thesis: verum end; now__::_thesis:_ex_M_being_Element_of_REAL_st_ (_M_>_0_&_(_for_n_being_Element_of_NAT_holds_||.(seq2_._n).||_<=_M_)_) consider M2 being Real such that A9: M2 > 0 and A10: for n being Element of NAT st n <= m1 holds ||.(seq2 . n).|| < M2 by Th23; consider M1 being Real such that A11: M1 > 0 and A12: for n being Element of NAT st n >= m1 holds ||.(seq2 . n).|| < M1 by A6; take M = M1 + M2; ::_thesis: ( M > 0 & ( for n being Element of NAT holds ||.(seq2 . n).|| <= M ) ) thus M > 0 by A11, A9; ::_thesis: for n being Element of NAT holds ||.(seq2 . n).|| <= M let n be Element of NAT ; ::_thesis: ||.(seq2 . n).|| <= M A13: M > 0 + M2 by A11, XREAL_1:8; A14: now__::_thesis:_(_n_<=_m1_implies_||.(seq2_._n).||_<=_M_) assume n <= m1 ; ::_thesis: ||.(seq2 . n).|| <= M then ||.(seq2 . n).|| < M2 by A10; hence ||.(seq2 . n).|| <= M by A13, XXREAL_0:2; ::_thesis: verum end; A15: M > M1 + 0 by A9, XREAL_1:8; now__::_thesis:_(_n_>=_m1_implies_||.(seq2_._n).||_<=_M_) assume n >= m1 ; ::_thesis: ||.(seq2 . n).|| <= M then ||.(seq2 . n).|| < M1 by A12; hence ||.(seq2 . n).|| <= M by A15, XXREAL_0:2; ::_thesis: verum end; hence ||.(seq2 . n).|| <= M by A14; ::_thesis: verum end; hence seq2 is bounded by Def3; ::_thesis: verum end; theorem Th26: :: BHSP_3:26 for X being RealUnitarySpace for seq, seq1 being sequence of X st seq is bounded & seq1 is subsequence of seq holds seq1 is bounded proof let X be RealUnitarySpace; ::_thesis: for seq, seq1 being sequence of X st seq is bounded & seq1 is subsequence of seq holds seq1 is bounded let seq, seq1 be sequence of X; ::_thesis: ( seq is bounded & seq1 is subsequence of seq implies seq1 is bounded ) assume that A1: seq is bounded and A2: seq1 is subsequence of seq ; ::_thesis: seq1 is bounded consider Nseq being increasing sequence of NAT such that A3: seq1 = seq * Nseq by A2, VALUED_0:def_17; consider M1 being Real such that A4: M1 > 0 and A5: for n being Element of NAT holds ||.(seq . n).|| <= M1 by A1, Def3; take M = M1; :: according to BHSP_3:def_3 ::_thesis: ( M > 0 & ( for n being Element of NAT holds ||.(seq1 . n).|| <= M ) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_||.(seq1_._n).||_<=_M let n be Element of NAT ; ::_thesis: ||.(seq1 . n).|| <= M seq1 . n = seq . (Nseq . n) by A3, FUNCT_2:15; hence ||.(seq1 . n).|| <= M by A5; ::_thesis: verum end; hence ( M > 0 & ( for n being Element of NAT holds ||.(seq1 . n).|| <= M ) ) by A4; ::_thesis: verum end; theorem Th27: :: BHSP_3:27 for X being RealUnitarySpace for seq, seq1 being sequence of X st seq is convergent & seq1 is subsequence of seq holds seq1 is convergent proof let X be RealUnitarySpace; ::_thesis: for seq, seq1 being sequence of X st seq is convergent & seq1 is subsequence of seq holds seq1 is convergent let seq, seq1 be sequence of X; ::_thesis: ( seq is convergent & seq1 is subsequence of seq implies seq1 is convergent ) assume that A1: seq is convergent and A2: seq1 is subsequence of seq ; ::_thesis: seq1 is convergent consider g1 being Point of X such that A3: for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq . n) - g1).|| < r by A1, BHSP_2:9; consider Nseq being increasing sequence of NAT such that A4: seq1 = seq * Nseq by A2, VALUED_0:def_17; now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_m_holds_ ||.((seq1_._n)_-_g1).||_<_r let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - g1).|| < r ) assume r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - g1).|| < r then consider m1 being Element of NAT such that A5: for n being Element of NAT st n >= m1 holds ||.((seq . n) - g1).|| < r by A3; take m = m1; ::_thesis: for n being Element of NAT st n >= m holds ||.((seq1 . n) - g1).|| < r let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((seq1 . n) - g1).|| < r ) assume A6: n >= m ; ::_thesis: ||.((seq1 . n) - g1).|| < r Nseq . n >= n by SEQM_3:14; then A7: Nseq . n >= m by A6, XXREAL_0:2; seq1 . n = seq . (Nseq . n) by A4, FUNCT_2:15; hence ||.((seq1 . n) - g1).|| < r by A5, A7; ::_thesis: verum end; hence seq1 is convergent by BHSP_2:9; ::_thesis: verum end; theorem Th28: :: BHSP_3:28 for X being RealUnitarySpace for seq1, seq being sequence of X st seq1 is subsequence of seq & seq is convergent holds lim seq1 = lim seq proof let X be RealUnitarySpace; ::_thesis: for seq1, seq being sequence of X st seq1 is subsequence of seq & seq is convergent holds lim seq1 = lim seq let seq1, seq be sequence of X; ::_thesis: ( seq1 is subsequence of seq & seq is convergent implies lim seq1 = lim seq ) assume that A1: seq1 is subsequence of seq and A2: seq is convergent ; ::_thesis: lim seq1 = lim seq consider Nseq being increasing sequence of NAT such that A3: seq1 = seq * Nseq by A1, VALUED_0:def_17; A4: now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_m_holds_ dist_((seq1_._n),(lim_seq))_<_r let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq1 . n),(lim seq)) < r ) assume r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds dist ((seq1 . n),(lim seq)) < r then consider m1 being Element of NAT such that A5: for n being Element of NAT st n >= m1 holds dist ((seq . n),(lim seq)) < r by A2, BHSP_2:def_2; take m = m1; ::_thesis: for n being Element of NAT st n >= m holds dist ((seq1 . n),(lim seq)) < r let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq1 . n),(lim seq)) < r ) assume A6: n >= m ; ::_thesis: dist ((seq1 . n),(lim seq)) < r Nseq . n >= n by SEQM_3:14; then A7: Nseq . n >= m by A6, XXREAL_0:2; seq1 . n = seq . (Nseq . n) by A3, FUNCT_2:15; hence dist ((seq1 . n),(lim seq)) < r by A5, A7; ::_thesis: verum end; seq1 is convergent by A1, A2, Th27; hence lim seq1 = lim seq by A4, BHSP_2:def_2; ::_thesis: verum end; theorem Th29: :: BHSP_3:29 for X being RealUnitarySpace for seq, seq1 being sequence of X st seq is Cauchy & seq1 is subsequence of seq holds seq1 is Cauchy proof let X be RealUnitarySpace; ::_thesis: for seq, seq1 being sequence of X st seq is Cauchy & seq1 is subsequence of seq holds seq1 is Cauchy let seq, seq1 be sequence of X; ::_thesis: ( seq is Cauchy & seq1 is subsequence of seq implies seq1 is Cauchy ) assume that A1: seq is Cauchy and A2: seq1 is subsequence of seq ; ::_thesis: seq1 is Cauchy consider Nseq being increasing sequence of NAT such that A3: seq1 = seq * Nseq by A2, VALUED_0:def_17; now__::_thesis:_for_r_being_Real_st_r_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_ dist_((seq1_._n),(seq1_._m))_<_r let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist ((seq1 . n),(seq1 . m)) < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist ((seq1 . n),(seq1 . m)) < r then consider l being Element of NAT such that A4: for n, m being Element of NAT st n >= l & m >= l holds dist ((seq . n),(seq . m)) < r by A1, Def1; take k = l; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds dist ((seq1 . n),(seq1 . m)) < r let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist ((seq1 . n),(seq1 . m)) < r ) assume that A5: n >= k and A6: m >= k ; ::_thesis: dist ((seq1 . n),(seq1 . m)) < r Nseq . n >= n by SEQM_3:14; then A7: Nseq . n >= k by A5, XXREAL_0:2; Nseq . m >= m by SEQM_3:14; then A8: Nseq . m >= k by A6, XXREAL_0:2; ( seq1 . n = seq . (Nseq . n) & seq1 . m = seq . (Nseq . m) ) by A3, FUNCT_2:15; hence dist ((seq1 . n),(seq1 . m)) < r by A4, A7, A8; ::_thesis: verum end; hence seq1 is Cauchy by Def1; ::_thesis: verum end; theorem :: BHSP_3:30 for X being RealUnitarySpace for seq being sequence of X for k, m being Element of NAT holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k proof let X be RealUnitarySpace; ::_thesis: for seq being sequence of X for k, m being Element of NAT holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k let seq be sequence of X; ::_thesis: for k, m being Element of NAT holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k let k, m be Element of NAT ; ::_thesis: (seq ^\ k) ^\ m = (seq ^\ m) ^\ k now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_^\_k)_^\_m)_._n_=_((seq_^\_m)_^\_k)_._n let n be Element of NAT ; ::_thesis: ((seq ^\ k) ^\ m) . n = ((seq ^\ m) ^\ k) . n thus ((seq ^\ k) ^\ m) . n = (seq ^\ k) . (n + m) by NAT_1:def_3 .= seq . ((n + m) + k) by NAT_1:def_3 .= seq . ((n + k) + m) .= (seq ^\ m) . (n + k) by NAT_1:def_3 .= ((seq ^\ m) ^\ k) . n by NAT_1:def_3 ; ::_thesis: verum end; hence (seq ^\ k) ^\ m = (seq ^\ m) ^\ k by FUNCT_2:63; ::_thesis: verum end; theorem :: BHSP_3:31 for X being RealUnitarySpace for seq being sequence of X for k, m being Element of NAT holds (seq ^\ k) ^\ m = seq ^\ (k + m) proof let X be RealUnitarySpace; ::_thesis: for seq being sequence of X for k, m being Element of NAT holds (seq ^\ k) ^\ m = seq ^\ (k + m) let seq be sequence of X; ::_thesis: for k, m being Element of NAT holds (seq ^\ k) ^\ m = seq ^\ (k + m) let k, m be Element of NAT ; ::_thesis: (seq ^\ k) ^\ m = seq ^\ (k + m) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_^\_k)_^\_m)_._n_=_(seq_^\_(k_+_m))_._n let n be Element of NAT ; ::_thesis: ((seq ^\ k) ^\ m) . n = (seq ^\ (k + m)) . n thus ((seq ^\ k) ^\ m) . n = (seq ^\ k) . (n + m) by NAT_1:def_3 .= seq . ((n + m) + k) by NAT_1:def_3 .= seq . (n + (k + m)) .= (seq ^\ (k + m)) . n by NAT_1:def_3 ; ::_thesis: verum end; hence (seq ^\ k) ^\ m = seq ^\ (k + m) by FUNCT_2:63; ::_thesis: verum end; theorem Th32: :: BHSP_3:32 for X being RealUnitarySpace for seq1, seq2 being sequence of X for k being Element of NAT holds (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k) proof let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X for k being Element of NAT holds (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k) let seq1, seq2 be sequence of X; ::_thesis: for k being Element of NAT holds (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k) let k be Element of NAT ; ::_thesis: (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_^\_k)_._n_=_((seq1_^\_k)_+_(seq2_^\_k))_._n let n be Element of NAT ; ::_thesis: ((seq1 + seq2) ^\ k) . n = ((seq1 ^\ k) + (seq2 ^\ k)) . n thus ((seq1 + seq2) ^\ k) . n = (seq1 + seq2) . (n + k) by NAT_1:def_3 .= (seq1 . (n + k)) + (seq2 . (n + k)) by NORMSP_1:def_2 .= ((seq1 ^\ k) . n) + (seq2 . (n + k)) by NAT_1:def_3 .= ((seq1 ^\ k) . n) + ((seq2 ^\ k) . n) by NAT_1:def_3 .= ((seq1 ^\ k) + (seq2 ^\ k)) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k) by FUNCT_2:63; ::_thesis: verum end; theorem Th33: :: BHSP_3:33 for X being RealUnitarySpace for seq being sequence of X for k being Element of NAT holds (- seq) ^\ k = - (seq ^\ k) proof let X be RealUnitarySpace; ::_thesis: for seq being sequence of X for k being Element of NAT holds (- seq) ^\ k = - (seq ^\ k) let seq be sequence of X; ::_thesis: for k being Element of NAT holds (- seq) ^\ k = - (seq ^\ k) let k be Element of NAT ; ::_thesis: (- seq) ^\ k = - (seq ^\ k) now__::_thesis:_for_n_being_Element_of_NAT_holds_((-_seq)_^\_k)_._n_=_(-_(seq_^\_k))_._n let n be Element of NAT ; ::_thesis: ((- seq) ^\ k) . n = (- (seq ^\ k)) . n thus ((- seq) ^\ k) . n = (- seq) . (n + k) by NAT_1:def_3 .= - (seq . (n + k)) by BHSP_1:44 .= - ((seq ^\ k) . n) by NAT_1:def_3 .= (- (seq ^\ k)) . n by BHSP_1:44 ; ::_thesis: verum end; hence (- seq) ^\ k = - (seq ^\ k) by FUNCT_2:63; ::_thesis: verum end; theorem :: BHSP_3:34 for X being RealUnitarySpace for seq1, seq2 being sequence of X for k being Element of NAT holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k) proof let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X for k being Element of NAT holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k) let seq1, seq2 be sequence of X; ::_thesis: for k being Element of NAT holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k) let k be Element of NAT ; ::_thesis: (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k) thus (seq1 - seq2) ^\ k = (seq1 + (- seq2)) ^\ k by BHSP_1:49 .= (seq1 ^\ k) + ((- seq2) ^\ k) by Th32 .= (seq1 ^\ k) + (- (seq2 ^\ k)) by Th33 .= (seq1 ^\ k) - (seq2 ^\ k) by BHSP_1:49 ; ::_thesis: verum end; theorem :: BHSP_3:35 for X being RealUnitarySpace for a being Real for seq being sequence of X for k being Element of NAT holds (a * seq) ^\ k = a * (seq ^\ k) proof let X be RealUnitarySpace; ::_thesis: for a being Real for seq being sequence of X for k being Element of NAT holds (a * seq) ^\ k = a * (seq ^\ k) let a be Real; ::_thesis: for seq being sequence of X for k being Element of NAT holds (a * seq) ^\ k = a * (seq ^\ k) let seq be sequence of X; ::_thesis: for k being Element of NAT holds (a * seq) ^\ k = a * (seq ^\ k) let k be Element of NAT ; ::_thesis: (a * seq) ^\ k = a * (seq ^\ k) now__::_thesis:_for_n_being_Element_of_NAT_holds_((a_*_seq)_^\_k)_._n_=_(a_*_(seq_^\_k))_._n let n be Element of NAT ; ::_thesis: ((a * seq) ^\ k) . n = (a * (seq ^\ k)) . n thus ((a * seq) ^\ k) . n = (a * seq) . (n + k) by NAT_1:def_3 .= a * (seq . (n + k)) by NORMSP_1:def_5 .= a * ((seq ^\ k) . n) by NAT_1:def_3 .= (a * (seq ^\ k)) . n by NORMSP_1:def_5 ; ::_thesis: verum end; hence (a * seq) ^\ k = a * (seq ^\ k) by FUNCT_2:63; ::_thesis: verum end; theorem :: BHSP_3:36 for X being RealUnitarySpace for seq being sequence of X for k being Element of NAT st seq is convergent holds ( seq ^\ k is convergent & lim (seq ^\ k) = lim seq ) by Th27, Th28; theorem :: BHSP_3:37 for X being RealUnitarySpace for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds seq1 is convergent proof let X be RealUnitarySpace; ::_thesis: for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds seq1 is convergent let seq, seq1 be sequence of X; ::_thesis: ( seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k implies seq1 is convergent ) assume that A1: seq is convergent and A2: ex k being Element of NAT st seq = seq1 ^\ k ; ::_thesis: seq1 is convergent consider k being Element of NAT such that A3: seq = seq1 ^\ k by A2; consider g1 being Point of X such that A4: for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq . n) - g1).|| < r by A1, BHSP_2:9; now__::_thesis:_ex_g_being_Point_of_X_st_ for_r_being_Real_st_r_>_0_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_m_holds_ ||.((seq1_._n)_-_g).||_<_r take g = g1; ::_thesis: for r being Real st r > 0 holds ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - g).|| < r let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - g).|| < r ) assume r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds ||.((seq1 . n) - g).|| < r then consider m1 being Element of NAT such that A5: for n being Element of NAT st n >= m1 holds ||.((seq . n) - g).|| < r by A4; take m = m1 + k; ::_thesis: for n being Element of NAT st n >= m holds ||.((seq1 . n) - g).|| < r let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((seq1 . n) - g).|| < r ) assume A6: n >= m ; ::_thesis: ||.((seq1 . n) - g).|| < r then consider m2 being Nat such that A7: n = (m1 + k) + m2 by NAT_1:10; reconsider m2 = m2 as Element of NAT by ORDINAL1:def_12; n - k = m1 + m2 by A7; then consider l being Element of NAT such that A8: l = n - k ; now__::_thesis:_not_l_<_m1 assume l < m1 ; ::_thesis: contradiction then l + k < m1 + k by XREAL_1:6; hence contradiction by A6, A8; ::_thesis: verum end; then A9: ||.((seq . l) - g).|| < r by A5; l + k = n by A8; hence ||.((seq1 . n) - g).|| < r by A3, A9, NAT_1:def_3; ::_thesis: verum end; hence seq1 is convergent by BHSP_2:9; ::_thesis: verum end; theorem :: BHSP_3:38 for X being RealUnitarySpace for seq, seq1 being sequence of X st seq is Cauchy & ex k being Element of NAT st seq = seq1 ^\ k holds seq1 is Cauchy proof let X be RealUnitarySpace; ::_thesis: for seq, seq1 being sequence of X st seq is Cauchy & ex k being Element of NAT st seq = seq1 ^\ k holds seq1 is Cauchy let seq, seq1 be sequence of X; ::_thesis: ( seq is Cauchy & ex k being Element of NAT st seq = seq1 ^\ k implies seq1 is Cauchy ) assume that A1: seq is Cauchy and A2: ex k being Element of NAT st seq = seq1 ^\ k ; ::_thesis: seq1 is Cauchy consider k being Element of NAT such that A3: seq = seq1 ^\ k by A2; let r be Real; :: according to BHSP_3:def_1 ::_thesis: ( r > 0 implies ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist ((seq1 . n),(seq1 . m)) < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds dist ((seq1 . n),(seq1 . m)) < r then consider l1 being Element of NAT such that A4: for n, m being Element of NAT st n >= l1 & m >= l1 holds dist ((seq . n),(seq . m)) < r by A1, Def1; take l = l1 + k; ::_thesis: for n, m being Element of NAT st n >= l & m >= l holds dist ((seq1 . n),(seq1 . m)) < r let n, m be Element of NAT ; ::_thesis: ( n >= l & m >= l implies dist ((seq1 . n),(seq1 . m)) < r ) assume that A5: n >= l and A6: m >= l ; ::_thesis: dist ((seq1 . n),(seq1 . m)) < r consider m1 being Nat such that A7: n = (l1 + k) + m1 by A5, NAT_1:10; reconsider m1 = m1 as Element of NAT by ORDINAL1:def_12; n - k = l1 + m1 by A7; then consider l2 being Element of NAT such that A8: l2 = n - k ; consider m2 being Nat such that A9: m = (l1 + k) + m2 by A6, NAT_1:10; reconsider m2 = m2 as Element of NAT by ORDINAL1:def_12; m - k = l1 + m2 by A9; then consider l3 being Element of NAT such that A10: l3 = m - k ; A11: now__::_thesis:_not_l2_<_l1 assume l2 < l1 ; ::_thesis: contradiction then l2 + k < l1 + k by XREAL_1:6; hence contradiction by A5, A8; ::_thesis: verum end; A12: l2 + k = n by A8; now__::_thesis:_not_l3_<_l1 assume l3 < l1 ; ::_thesis: contradiction then l3 + k < l1 + k by XREAL_1:6; hence contradiction by A6, A10; ::_thesis: verum end; then dist ((seq . l2),(seq . l3)) < r by A4, A11; then A13: dist ((seq1 . n),(seq . l3)) < r by A3, A12, NAT_1:def_3; l3 + k = m by A10; hence dist ((seq1 . n),(seq1 . m)) < r by A3, A13, NAT_1:def_3; ::_thesis: verum end; theorem :: BHSP_3:39 for X being RealUnitarySpace for seq being sequence of X for k being Element of NAT st seq is Cauchy holds seq ^\ k is Cauchy by Th29; theorem :: BHSP_3:40 for X being RealUnitarySpace for seq1, seq2 being sequence of X for k being Element of NAT st seq1 is_compared_to seq2 holds seq1 ^\ k is_compared_to seq2 ^\ k proof let X be RealUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X for k being Element of NAT st seq1 is_compared_to seq2 holds seq1 ^\ k is_compared_to seq2 ^\ k let seq1, seq2 be sequence of X; ::_thesis: for k being Element of NAT st seq1 is_compared_to seq2 holds seq1 ^\ k is_compared_to seq2 ^\ k let k be Element of NAT ; ::_thesis: ( seq1 is_compared_to seq2 implies seq1 ^\ k is_compared_to seq2 ^\ k ) assume A1: seq1 is_compared_to seq2 ; ::_thesis: seq1 ^\ k is_compared_to seq2 ^\ k let r be Real; :: according to BHSP_3:def_2 ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r ) assume r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r then consider m1 being Element of NAT such that A2: for n being Element of NAT st n >= m1 holds dist ((seq1 . n),(seq2 . n)) < r by A1, Def2; take m = m1; ::_thesis: for n being Element of NAT st n >= m holds dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r let n be Element of NAT ; ::_thesis: ( n >= m implies dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r ) assume A3: n >= m ; ::_thesis: dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r n + k >= n by NAT_1:11; then n + k >= m by A3, XXREAL_0:2; then dist ((seq1 . (n + k)),(seq2 . (n + k))) < r by A2; then dist (((seq1 ^\ k) . n),(seq2 . (n + k))) < r by NAT_1:def_3; hence dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r by NAT_1:def_3; ::_thesis: verum end; theorem :: BHSP_3:41 for X being RealUnitarySpace for seq being sequence of X for k being Element of NAT st seq is bounded holds seq ^\ k is bounded by Th26; theorem :: BHSP_3:42 for X being RealUnitarySpace for seq being sequence of X for k being Element of NAT st seq is constant holds seq ^\ k is constant ; definition let X be RealUnitarySpace; attrX is complete means :Def4: :: BHSP_3:def 4 for seq being sequence of X st seq is Cauchy holds seq is convergent ; end; :: deftheorem Def4 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 ); 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 proof let X be RealUnitarySpace; ::_thesis: for seq being sequence of X st X is complete & seq is Cauchy holds seq is bounded let seq be sequence of X; ::_thesis: ( X is complete & seq is Cauchy implies seq is bounded ) assume ( X is complete & seq is Cauchy ) ; ::_thesis: seq is bounded then seq is convergent by Def4; hence seq is bounded by Th24; ::_thesis: verum end;