let M be non empty Reflexive MetrStruct ; :: thesis: for S being bounded SetSequence of M st S is non-ascending & lim (diameter S) = 0 holds
for F being sequence of M st ( for i being natural number holds F . i in S . i ) holds
F is Cauchy
let S be bounded SetSequence of M; :: thesis: ( S is non-ascending & lim (diameter S) = 0 implies for F being sequence of M st ( for i being natural number holds F . i in S . i ) holds
F is Cauchy )
assume A1: ( S is non-ascending & lim (diameter S) = 0 ) ; :: thesis: for F being sequence of M st ( for i being natural number holds F . i in S . i ) holds
F is Cauchy
set d = diameter S;
let F be sequence of M; :: thesis: ( ( for i being natural number holds F . i in S . i ) implies F is Cauchy )
assume A2: for i being natural number holds F . i in S . i ; :: thesis: F is Cauchy
let r be Real; :: according to TBSP_1:def 5 :: thesis: ( r <= 0 or ex b₁ being Element of NAT st
for b₂, b₃ being Element of NAT holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist (F . b₂),(F . b₃) ) )
assume A3: r > 0 ; :: thesis: ex b₁ being Element of NAT st
for b₂, b₃ being Element of NAT holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist (F . b₂),(F . b₃) )
( diameter S is bounded_below & diameter S is non-increasing ) by A1, Th1, Th2;
then consider n being Element of NAT such that
A4: for m being Element of NAT st n <= m holds
abs (((diameter S) . m) - 0 ) < r by A1, A3, SEQ_2:def 7;
take n ; :: thesis: for b₁, b₂ being Element of NAT holds
( not n <= b₁ or not n <= b₂ or not r <= dist (F . b₁),(F . b₂) )
let m1, m2 be Element of NAT ; :: thesis: ( not n <= m1 or not n <= m2 or not r <= dist (F . m1),(F . m2) )
assume A5: ( n <= m1 & n <= m2 ) ; :: thesis: not r <= dist (F . m1),(F . m2)
( S . m1 c= S . n & S . m2 c= S . n & F . m1 in S . m1 & F . m2 in S . m2 ) by A1, A2, A5, PROB_1:def 6;
then ( F . m1 in S . n & F . m2 in S . n & S . n is bounded & diameter (S . n) = (diameter S) . n ) by Def1, Def2;
then A6: ( dist (F . m1),(F . m2) <= (diameter S) . n & 0 <= (diameter S) . n & abs (((diameter S) . n) - 0 ) < r ) by A4, TBSP_1:29, TBSP_1:def 10;
then (diameter S) . n < r by ABSVALUE:def 1;
hence not r <= dist (F . m1),(F . m2) by A6, XXREAL_0:2; :: thesis: verum