:: METRIC_6 semantic presentation begin theorem Th1: :: METRIC_6:1 for X being MetrSpace for x, z, y being Element of X holds abs ((dist (x,z)) - (dist (y,z))) <= dist (x,y) proof let X be MetrSpace; ::_thesis: for x, z, y being Element of X holds abs ((dist (x,z)) - (dist (y,z))) <= dist (x,y) let x, z, y be Element of X; ::_thesis: abs ((dist (x,z)) - (dist (y,z))) <= dist (x,y) dist (y,z) <= (dist (y,x)) + (dist (x,z)) by METRIC_1:4; then (dist (y,z)) - (dist (x,z)) <= dist (x,y) by XREAL_1:20; then A1: - (dist (x,y)) <= - ((dist (y,z)) - (dist (x,z))) by XREAL_1:24; dist (x,z) <= (dist (x,y)) + (dist (y,z)) by METRIC_1:4; then (dist (x,z)) - (dist (y,z)) <= dist (x,y) by XREAL_1:20; hence abs ((dist (x,z)) - (dist (y,z))) <= dist (x,y) by A1, ABSVALUE:5; ::_thesis: verum end; theorem Th2: :: METRIC_6:2 for A being non empty set for G being Function of [:A,A:],REAL st G is_metric_of A holds for a, b being Element of A holds 0 <= G . (a,b) proof let A be non empty set ; ::_thesis: for G being Function of [:A,A:],REAL st G is_metric_of A holds for a, b being Element of A holds 0 <= G . (a,b) let G be Function of [:A,A:],REAL; ::_thesis: ( G is_metric_of A implies for a, b being Element of A holds 0 <= G . (a,b) ) assume A1: G is_metric_of A ; ::_thesis: for a, b being Element of A holds 0 <= G . (a,b) let a, b be Element of A; ::_thesis: 0 <= G . (a,b) A2: (1 / 2) * (G . (a,a)) = (1 / 2) * 0 by A1, PCOMPS_1:def_6; G . (a,b) = (1 / 2) * ((1 * (G . (a,b))) + (G . (a,b))) .= (1 / 2) * ((G . (a,b)) + (G . (b,a))) by A1, PCOMPS_1:def_6 ; hence 0 <= G . (a,b) by A1, A2, PCOMPS_1:def_6; ::_thesis: verum end; theorem Th3: :: METRIC_6:3 for A being non empty set for G being Function of [:A,A:],REAL holds ( G is_metric_of A iff ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) ) proof let A be non empty set ; ::_thesis: for G being Function of [:A,A:],REAL holds ( G is_metric_of A iff ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) ) let G be Function of [:A,A:],REAL; ::_thesis: ( G is_metric_of A iff ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) ) A1: ( G is_metric_of A implies ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) ) proof assume A2: G is_metric_of A ; ::_thesis: ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) then for a being Element of A holds G . (a,a) = 0 by PCOMPS_1:def_6; hence G is Reflexive by METRIC_1:def_2; ::_thesis: ( G is discerning & G is symmetric & G is triangle ) for a, b being Element of A holds ( G . (a,b) = 0 iff a = b ) by A2, PCOMPS_1:def_6; hence G is discerning by METRIC_1:def_3; ::_thesis: ( G is symmetric & G is triangle ) for a, b being Element of A holds G . (a,b) = G . (b,a) by A2, PCOMPS_1:def_6; hence G is symmetric by METRIC_1:def_4; ::_thesis: G is triangle for a, b, c being Element of A holds G . (a,c) <= (G . (a,b)) + (G . (b,c)) by A2, PCOMPS_1:def_6; hence G is triangle by METRIC_1:def_5; ::_thesis: verum end; ( G is Reflexive & G is discerning & G is symmetric & G is triangle implies G is_metric_of A ) proof assume ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) ; ::_thesis: G is_metric_of A then for a, b, c being Element of A holds ( ( G . (a,b) = 0 implies a = b ) & ( a = b implies G . (a,b) = 0 ) & G . (a,b) = G . (b,a) & G . (a,c) <= (G . (a,b)) + (G . (b,c)) ) by METRIC_1:def_2, METRIC_1:def_3, METRIC_1:def_4, METRIC_1:def_5; hence G is_metric_of A by PCOMPS_1:def_6; ::_thesis: verum end; hence ( G is_metric_of A iff ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) ) by A1; ::_thesis: verum end; theorem :: METRIC_6:4 for X being non empty strict MetrSpace holds ( the distance of X is Reflexive & the distance of X is discerning & the distance of X is symmetric & the distance of X is triangle ) proof let X be non empty strict MetrSpace; ::_thesis: ( the distance of X is Reflexive & the distance of X is discerning & the distance of X is symmetric & the distance of X is triangle ) A1: the distance of X is_metric_of the carrier of X by PCOMPS_1:35; hence the distance of X is Reflexive by Th3; ::_thesis: ( the distance of X is discerning & the distance of X is symmetric & the distance of X is triangle ) thus the distance of X is discerning by A1, Th3; ::_thesis: ( the distance of X is symmetric & the distance of X is triangle ) thus the distance of X is symmetric by A1, Th3; ::_thesis: the distance of X is triangle thus the distance of X is triangle by A1, Th3; ::_thesis: verum end; theorem :: METRIC_6:5 for A being non empty set for G being Function of [:A,A:],REAL holds ( G is_metric_of A iff ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) ) ) proof let A be non empty set ; ::_thesis: for G being Function of [:A,A:],REAL holds ( G is_metric_of A iff ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) ) ) let G be Function of [:A,A:],REAL; ::_thesis: ( G is_metric_of A iff ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) ) ) A1: ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) implies G is_metric_of A ) proof assume that A2: ( G is Reflexive & G is discerning ) and A3: for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ; ::_thesis: G is_metric_of A A4: for b, c being Element of A holds G . (b,c) = G . (c,b) proof let b, c be Element of A; ::_thesis: G . (b,c) = G . (c,b) G . (c,b) <= (G . (b,c)) + (G . (b,b)) by A3; then A5: G . (c,b) <= (G . (b,c)) + 0 by A2, METRIC_1:def_2; G . (b,c) <= (G . (c,b)) + (G . (c,c)) by A3; then G . (b,c) <= (G . (c,b)) + 0 by A2, METRIC_1:def_2; hence G . (b,c) = G . (c,b) by A5, XXREAL_0:1; ::_thesis: verum end; for a, b, c being Element of A holds G . (a,c) <= (G . (a,b)) + (G . (b,c)) proof let a, b, c be Element of A; ::_thesis: G . (a,c) <= (G . (a,b)) + (G . (b,c)) G . (a,c) <= (G . (b,a)) + (G . (b,c)) by A3; hence G . (a,c) <= (G . (a,b)) + (G . (b,c)) by A4; ::_thesis: verum end; then ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) by A2, A4, METRIC_1:def_4, METRIC_1:def_5; hence G is_metric_of A by Th3; ::_thesis: verum end; ( G is_metric_of A implies ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) ) ) proof assume A6: G is_metric_of A ; ::_thesis: ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) ) then A7: ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) by Th3; now__::_thesis:_for_a,_b,_c_being_Element_of_A_holds_G_._(b,c)_<=_(G_._(a,b))_+_(G_._(a,c)) let a, b, c be Element of A; ::_thesis: G . (b,c) <= (G . (a,b)) + (G . (a,c)) G . (b,c) <= (G . (b,a)) + (G . (a,c)) by A7, METRIC_1:def_5; hence G . (b,c) <= (G . (a,b)) + (G . (a,c)) by A7, METRIC_1:def_4; ::_thesis: verum end; hence ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) ) by A6, Th3; ::_thesis: verum end; hence ( G is_metric_of A iff ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) ) ) by A1; ::_thesis: verum end; definition let A be non empty set ; let G be Function of [:A,A:],REAL; func bounded_metric (A,G) -> Function of [:A,A:],REAL means :Def1: :: METRIC_6:def 1 for a, b being Element of A holds it . (a,b) = (G . (a,b)) / (1 + (G . (a,b))); existence ex b1 being Function of [:A,A:],REAL st for a, b being Element of A holds b1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) proof deffunc H1( Element of A, Element of A) -> Element of REAL = (G . (\$1,\$2)) / (1 + (G . (\$1,\$2))); consider F being Function of [:A,A:],REAL such that A1: for a, b being Element of A holds F . (a,b) = H1(a,b) from BINOP_1:sch_4(); take F ; ::_thesis: for a, b being Element of A holds F . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) let a, b be Element of A; ::_thesis: F . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) thus F . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of [:A,A:],REAL st ( for a, b being Element of A holds b1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) & ( for a, b being Element of A holds b2 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) holds b1 = b2 proof let f1, f2 be Function of [:A,A:],REAL; ::_thesis: ( ( for a, b being Element of A holds f1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) & ( for a, b being Element of A holds f2 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) implies f1 = f2 ) assume that A2: for a, b being Element of A holds f1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) and A3: for a, b being Element of A holds f2 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ; ::_thesis: f1 = f2 for a, b being Element of A holds f1 . (a,b) = f2 . (a,b) proof let a, b be Element of A; ::_thesis: f1 . (a,b) = f2 . (a,b) f1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) by A2; hence f1 . (a,b) = f2 . (a,b) by A3; ::_thesis: verum end; hence f1 = f2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines bounded_metric METRIC_6:def_1_:_ for A being non empty set for G, b3 being Function of [:A,A:],REAL holds ( b3 = bounded_metric (A,G) iff for a, b being Element of A holds b3 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ); theorem :: METRIC_6:6 for A being non empty set for G being Function of [:A,A:],REAL st G is_metric_of A holds bounded_metric (A,G) is_metric_of A proof let A be non empty set ; ::_thesis: for G being Function of [:A,A:],REAL st G is_metric_of A holds bounded_metric (A,G) is_metric_of A let G be Function of [:A,A:],REAL; ::_thesis: ( G is_metric_of A implies bounded_metric (A,G) is_metric_of A ) assume A1: G is_metric_of A ; ::_thesis: bounded_metric (A,G) is_metric_of A A2: for a, b, c being Element of A holds (bounded_metric (A,G)) . (a,c) <= ((bounded_metric (A,G)) . (a,b)) + ((bounded_metric (A,G)) . (b,c)) proof let a, b, c be Element of A; ::_thesis: (bounded_metric (A,G)) . (a,c) <= ((bounded_metric (A,G)) . (a,b)) + ((bounded_metric (A,G)) . (b,c)) set a1 = G . (a,b); set a3 = G . (a,c); set a5 = G . (b,c); A3: ( (bounded_metric (A,G)) . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) & (bounded_metric (A,G)) . (a,c) = (G . (a,c)) / (1 + (G . (a,c))) ) by Def1; A4: (bounded_metric (A,G)) . (b,c) = (G . (b,c)) / (1 + (G . (b,c))) by Def1; A5: G . (a,c) >= 0 by A1, Th2; A6: ( 0 <= G . (a,b) & 0 <= G . (b,c) ) by A1, Th2; then A7: 0 <> (1 + (G . (a,b))) * (1 + (G . (b,c))) by XCMPLX_1:6; A8: ((G . (a,b)) / (1 + (G . (a,b)))) + ((G . (b,c)) / (1 + (G . (b,c)))) = (((G . (a,b)) * (1 + (G . (b,c)))) + ((G . (b,c)) * (1 + (G . (a,b))))) / ((1 + (G . (a,b))) * (1 + (G . (b,c)))) by A6, XCMPLX_1:116 .= ((((G . (a,b)) * 1) + ((G . (a,b)) * (G . (b,c)))) + (((G . (b,c)) * 1) + ((G . (b,c)) * (G . (a,b))))) / ((1 + (G . (a,b))) * (1 + (G . (b,c)))) ; 0 <= G . (a,c) by A1, Th2; then A9: (((G . (a,b)) / (1 + (G . (a,b)))) + ((G . (b,c)) / (1 + (G . (b,c))))) - ((G . (a,c)) / (1 + (G . (a,c)))) = (((((G . (a,b)) + ((G . (a,b)) * (G . (b,c)))) + ((G . (b,c)) + ((G . (b,c)) * (G . (a,b))))) * (1 + (G . (a,c)))) - ((G . (a,c)) * ((1 + (G . (a,b))) * (1 + (G . (b,c)))))) / (((1 + (G . (a,b))) * (1 + (G . (b,c)))) * (1 + (G . (a,c)))) by A7, A8, XCMPLX_1:130; A10: ( G . (a,b) >= 0 & G . (b,c) >= 0 ) by A1, Th2; G . (a,c) <= (G . (a,b)) + (G . (b,c)) by A1, PCOMPS_1:def_6; then ((G . (a,b)) + (G . (b,c))) - (G . (a,c)) >= 0 by XREAL_1:48; then (((G . (b,c)) + (G . (a,b))) - (G . (a,c))) + (((G . (a,b)) * (G . (b,c))) + (((G . (b,c)) * (G . (a,b))) + (((G . (b,c)) * (G . (a,b))) * (G . (a,c))))) >= 0 by A10, A5; hence (bounded_metric (A,G)) . (a,c) <= ((bounded_metric (A,G)) . (a,b)) + ((bounded_metric (A,G)) . (b,c)) by A3, A4, A9, A10, A5, XREAL_1:49; ::_thesis: verum end; A11: for a, b being Element of A holds ( (bounded_metric (A,G)) . (a,b) = 0 iff a = b ) proof let a, b be Element of A; ::_thesis: ( (bounded_metric (A,G)) . (a,b) = 0 iff a = b ) A12: ( (bounded_metric (A,G)) . (a,b) = 0 implies a = b ) proof assume (bounded_metric (A,G)) . (a,b) = 0 ; ::_thesis: a = b then A13: (G . (a,b)) / (1 + (G . (a,b))) = 0 by Def1; 0 <= G . (a,b) by A1, Th2; then G . (a,b) = 0 by A13, XCMPLX_1:50; hence a = b by A1, PCOMPS_1:def_6; ::_thesis: verum end; ( a = b implies (bounded_metric (A,G)) . (a,b) = 0 ) proof assume a = b ; ::_thesis: (bounded_metric (A,G)) . (a,b) = 0 then G . (a,b) = 0 by A1, PCOMPS_1:def_6; then (G . (a,b)) / (1 + (G . (a,b))) = 0 ; hence (bounded_metric (A,G)) . (a,b) = 0 by Def1; ::_thesis: verum end; hence ( (bounded_metric (A,G)) . (a,b) = 0 iff a = b ) by A12; ::_thesis: verum end; for a, b being Element of A holds (bounded_metric (A,G)) . (a,b) = (bounded_metric (A,G)) . (b,a) proof let a, b be Element of A; ::_thesis: (bounded_metric (A,G)) . (a,b) = (bounded_metric (A,G)) . (b,a) (G . (a,b)) / (1 + (G . (a,b))) = (G . (b,a)) / (1 + (G . (a,b))) by A1, PCOMPS_1:def_6 .= (G . (b,a)) / (1 + (G . (b,a))) by A1, PCOMPS_1:def_6 .= (bounded_metric (A,G)) . (b,a) by Def1 ; hence (bounded_metric (A,G)) . (a,b) = (bounded_metric (A,G)) . (b,a) by Def1; ::_thesis: verum end; hence bounded_metric (A,G) is_metric_of A by A11, A2, PCOMPS_1:def_6; ::_thesis: verum end; theorem Th7: :: METRIC_6:7 for X being non empty MetrSpace for x being Element of X ex S being sequence of X st rng S = {x} proof let X be non empty MetrSpace; ::_thesis: for x being Element of X ex S being sequence of X st rng S = {x} let x be Element of X; ::_thesis: ex S being sequence of X st rng S = {x} consider f being Function such that A1: dom f = NAT and A2: rng f = {x} by FUNCT_1:5; reconsider f = f as sequence of X by A1, A2, FUNCT_2:2; take f ; ::_thesis: rng f = {x} thus rng f = {x} by A2; ::_thesis: verum end; definition let X be non empty MetrStruct ; let S be sequence of X; let x be Element of X; predS is_convergent_in_metrspace_to x means :Def2: :: METRIC_6:def 2 for r being Real st 0 < r holds ex m being Element of NAT st for n being Element of NAT st m <= n holds dist ((S . n),x) < r; end; :: deftheorem Def2 defines is_convergent_in_metrspace_to METRIC_6:def_2_:_ for X being non empty MetrStruct for S being sequence of X for x being Element of X holds ( S is_convergent_in_metrspace_to x iff for r being Real st 0 < r holds ex m being Element of NAT st for n being Element of NAT st m <= n holds dist ((S . n),x) < r ); definition let X be non empty symmetric triangle MetrStruct ; let V be Subset of X; redefine attr V is bounded means :Def3: :: METRIC_6:def 3 ex r being Real ex x being Element of X st ( 0 < r & V c= Ball (x,r) ); compatibility ( V is bounded iff ex r being Real ex x being Element of X st ( 0 < r & V c= Ball (x,r) ) ) proof hereby ::_thesis: ( ex r being Real ex x being Element of X st ( 0 < r & V c= Ball (x,r) ) implies V is bounded ) assume A1: V is bounded ; ::_thesis: ex s being Element of REAL ex x being Element of X st ( 0 < s & V c= Ball (x,s) ) percases ( V <> {} or V = {} ) ; suppose V <> {} ; ::_thesis: ex s being Element of REAL ex x being Element of X st ( 0 < s & V c= Ball (x,s) ) then consider x being Element of X such that A2: x in V by SUBSET_1:4; consider r being Real such that A3: 0 < r and A4: for x, y being Element of X st x in V & y in V holds dist (x,y) <= r by A1, TBSP_1:def_7; take s = 2 * r; ::_thesis: ex x being Element of X st ( 0 < s & V c= Ball (x,s) ) take x = x; ::_thesis: ( 0 < s & V c= Ball (x,s) ) thus 0 < s by A3, XREAL_1:129; ::_thesis: V c= Ball (x,s) thus V c= Ball (x,s) ::_thesis: verum proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in V or u in Ball (x,s) ) assume A5: u in V ; ::_thesis: u in Ball (x,s) then reconsider v = u as Element of X ; A6: 1 * r < s by A3, XREAL_1:68; dist (x,v) <= r by A4, A2, A5; then dist (x,v) < s by A6, XXREAL_0:2; hence u in Ball (x,s) by METRIC_1:11; ::_thesis: verum end; end; supposeA7: V = {} ; ::_thesis: ex r being Element of REAL ex x being Element of X st ( 0 < r & V c= Ball (x,r) ) set x = the Element of X; take r = 1 / 2; ::_thesis: ex x being Element of X st ( 0 < r & V c= Ball (x,r) ) take x = the Element of X; ::_thesis: ( 0 < r & V c= Ball (x,r) ) thus ( 0 < r & V c= Ball (x,r) ) by A7, XBOOLE_1:2; ::_thesis: verum end; end; end; given r being Real, x being Element of X such that A8: 0 < r and A9: V c= Ball (x,r) ; ::_thesis: V is bounded take 2 * r ; :: according to TBSP_1:def_7 ::_thesis: ( not 2 * r <= 0 & ( for b1, b2 being Element of the carrier of X holds ( not b1 in V or not b2 in V or dist (b1,b2) <= 2 * r ) ) ) thus 2 * r > 0 by A8, XREAL_1:129; ::_thesis: for b1, b2 being Element of the carrier of X holds ( not b1 in V or not b2 in V or dist (b1,b2) <= 2 * r ) let z, y be Element of X; ::_thesis: ( not z in V or not y in V or dist (z,y) <= 2 * r ) assume A10: z in V ; ::_thesis: ( not y in V or dist (z,y) <= 2 * r ) assume y in V ; ::_thesis: dist (z,y) <= 2 * r then A11: dist (x,y) < r by A9, METRIC_1:11; dist (x,z) < r by A9, A10, METRIC_1:11; then A12: (dist (z,x)) + (dist (x,y)) <= r + r by A11, XREAL_1:7; dist (z,y) <= (dist (z,x)) + (dist (x,y)) by METRIC_1:4; hence dist (z,y) <= 2 * r by A12, XXREAL_0:2; ::_thesis: verum end; end; :: deftheorem Def3 defines bounded METRIC_6:def_3_:_ for X being non empty symmetric triangle MetrStruct for V being Subset of X holds ( V is bounded iff ex r being Real ex x being Element of X st ( 0 < r & V c= Ball (x,r) ) ); definition let X be non empty MetrStruct ; let S be sequence of X; attrS is bounded means :Def4: :: METRIC_6:def 4 ex r being Real ex x being Element of X st ( 0 < r & rng S c= Ball (x,r) ); end; :: deftheorem Def4 defines bounded METRIC_6:def_4_:_ for X being non empty MetrStruct for S being sequence of X holds ( S is bounded iff ex r being Real ex x being Element of X st ( 0 < r & rng S c= Ball (x,r) ) ); definition let X be non empty MetrSpace; let V be Subset of X; let S be sequence of X; predV contains_almost_all_sequence S means :Def5: :: METRIC_6:def 5 ex m being Element of NAT st for n being Element of NAT st m <= n holds S . n in V; end; :: deftheorem Def5 defines contains_almost_all_sequence METRIC_6:def_5_:_ for X being non empty MetrSpace for V being Subset of X for S being sequence of X holds ( V contains_almost_all_sequence S iff ex m being Element of NAT st for n being Element of NAT st m <= n holds S . n in V ); theorem Th8: :: METRIC_6:8 for X being non empty MetrSpace for S being sequence of X holds ( S is bounded iff ex r being Real ex x being Element of X st ( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) ) proof let X be non empty MetrSpace; ::_thesis: for S being sequence of X holds ( S is bounded iff ex r being Real ex x being Element of X st ( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) ) let S be sequence of X; ::_thesis: ( S is bounded iff ex r being Real ex x being Element of X st ( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) ) thus ( S is bounded implies ex r being Real ex x being Element of X st ( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) ) ::_thesis: ( ex r being Real ex x being Element of X st ( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) implies S is bounded ) proof assume S is bounded ; ::_thesis: ex r being Real ex x being Element of X st ( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) then consider r being Real, x being Element of X such that A1: 0 < r and A2: rng S c= Ball (x,r) by Def4; take q = r; ::_thesis: ex x being Element of X st ( 0 < q & ( for n being Element of NAT holds S . n in Ball (x,q) ) ) take y = x; ::_thesis: ( 0 < q & ( for n being Element of NAT holds S . n in Ball (y,q) ) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_S_._n_in_Ball_(y,q) let n be Element of NAT ; ::_thesis: S . n in Ball (y,q) S . n in rng S by FUNCT_2:4; hence S . n in Ball (y,q) by A2; ::_thesis: verum end; hence ( 0 < q & ( for n being Element of NAT holds S . n in Ball (y,q) ) ) by A1; ::_thesis: verum end; thus ( ex r being Real ex x being Element of X st ( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) implies S is bounded ) ::_thesis: verum proof given r being Real, x being Element of X such that A3: 0 < r and A4: for n being Element of NAT holds S . n in Ball (x,r) ; ::_thesis: S is bounded for x1 being set st x1 in rng S holds x1 in Ball (x,r) proof let x1 be set ; ::_thesis: ( x1 in rng S implies x1 in Ball (x,r) ) assume x1 in rng S ; ::_thesis: x1 in Ball (x,r) then consider x2 being set such that A5: x2 in dom S and A6: x1 = S . x2 by FUNCT_1:def_3; x2 in NAT by A5, FUNCT_2:def_1; hence x1 in Ball (x,r) by A4, A6; ::_thesis: verum end; then rng S c= Ball (x,r) by TARSKI:def_3; hence S is bounded by A3, Def4; ::_thesis: verum end; end; theorem Th9: :: METRIC_6:9 for X being non empty MetrSpace for x being Element of X for S being sequence of X st S is_convergent_in_metrspace_to x holds S is convergent proof let X be non empty MetrSpace; ::_thesis: for x being Element of X for S being sequence of X st S is_convergent_in_metrspace_to x holds S is convergent let x be Element of X; ::_thesis: for S being sequence of X st S is_convergent_in_metrspace_to x holds S is convergent let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x implies S is convergent ) assume A1: S is_convergent_in_metrspace_to x ; ::_thesis: S is convergent take x ; :: according to TBSP_1:def_2 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= dist ((S . b3),x) ) ) thus for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= dist ((S . b3),x) ) ) by A1, Def2; ::_thesis: verum end; theorem Th10: :: METRIC_6:10 for X being non empty MetrSpace for S being sequence of X st S is convergent holds ex x being Element of X st S is_convergent_in_metrspace_to x proof let X be non empty MetrSpace; ::_thesis: for S being sequence of X st S is convergent holds ex x being Element of X st S is_convergent_in_metrspace_to x let S be sequence of X; ::_thesis: ( S is convergent implies ex x being Element of X st S is_convergent_in_metrspace_to x ) assume S is convergent ; ::_thesis: ex x being Element of X st S is_convergent_in_metrspace_to x then consider x being Element of X such that A1: for r being Real st 0 < r holds ex m being Element of NAT st for n being Element of NAT st m <= n holds dist ((S . n),x) < r by TBSP_1:def_2; S is_convergent_in_metrspace_to x by A1, Def2; hence ex x being Element of X st S is_convergent_in_metrspace_to x ; ::_thesis: verum end; definition let X be non empty MetrSpace; let S be sequence of X; let x be Element of X; func dist_to_point (S,x) -> Real_Sequence means :Def6: :: METRIC_6:def 6 for n being Element of NAT holds it . n = dist ((S . n),x); existence ex b1 being Real_Sequence st for n being Element of NAT holds b1 . n = dist ((S . n),x) proof deffunc H1( Element of NAT ) -> Element of REAL = dist ((S . \$1),x); consider seq being Real_Sequence such that A1: for n being Element of NAT holds seq . n = H1(n) from SEQ_1:sch_1(); take seq ; ::_thesis: for n being Element of NAT holds seq . n = dist ((S . n),x) thus for n being Element of NAT holds seq . n = dist ((S . n),x) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = dist ((S . n),x) ) & ( for n being Element of NAT holds b2 . n = dist ((S . n),x) ) holds b1 = b2 proof let seq1, seq2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = dist ((S . n),x) ) & ( for n being Element of NAT holds seq2 . n = dist ((S . n),x) ) implies seq1 = seq2 ) assume that A2: for n being Element of NAT holds seq1 . n = dist ((S . n),x) and A3: for n being Element of NAT holds seq2 . n = dist ((S . n),x) ; ::_thesis: seq1 = seq2 now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_seq2_._n let n be Element of NAT ; ::_thesis: seq1 . n = seq2 . n seq1 . n = dist ((S . n),x) by A2; hence seq1 . n = seq2 . n by A3; ::_thesis: verum end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def6 defines dist_to_point METRIC_6:def_6_:_ for X being non empty MetrSpace for S being sequence of X for x being Element of X for b4 being Real_Sequence holds ( b4 = dist_to_point (S,x) iff for n being Element of NAT holds b4 . n = dist ((S . n),x) ); definition let X be non empty MetrSpace; let S, T be sequence of X; func sequence_of_dist (S,T) -> Real_Sequence means :Def7: :: METRIC_6:def 7 for n being Element of NAT holds it . n = dist ((S . n),(T . n)); existence ex b1 being Real_Sequence st for n being Element of NAT holds b1 . n = dist ((S . n),(T . n)) proof deffunc H1( Element of NAT ) -> Element of REAL = dist ((S . \$1),(T . \$1)); consider seq being Real_Sequence such that A1: for n being Element of NAT holds seq . n = H1(n) from SEQ_1:sch_1(); take seq ; ::_thesis: for n being Element of NAT holds seq . n = dist ((S . n),(T . n)) thus for n being Element of NAT holds seq . n = dist ((S . n),(T . n)) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = dist ((S . n),(T . n)) ) & ( for n being Element of NAT holds b2 . n = dist ((S . n),(T . n)) ) holds b1 = b2 proof let seq1, seq2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = dist ((S . n),(T . n)) ) & ( for n being Element of NAT holds seq2 . n = dist ((S . n),(T . n)) ) implies seq1 = seq2 ) assume that A2: for n being Element of NAT holds seq1 . n = dist ((S . n),(T . n)) and A3: for n being Element of NAT holds seq2 . n = dist ((S . n),(T . n)) ; ::_thesis: seq1 = seq2 now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_seq2_._n let n be Element of NAT ; ::_thesis: seq1 . n = seq2 . n seq1 . n = dist ((S . n),(T . n)) by A2; hence seq1 . n = seq2 . n by A3; ::_thesis: verum end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def7 defines sequence_of_dist METRIC_6:def_7_:_ for X being non empty MetrSpace for S, T being sequence of X for b4 being Real_Sequence holds ( b4 = sequence_of_dist (S,T) iff for n being Element of NAT holds b4 . n = dist ((S . n),(T . n)) ); theorem Th11: :: METRIC_6:11 for X being non empty MetrSpace for x being Element of X for S being sequence of X st S is_convergent_in_metrspace_to x holds lim S = x proof let X be non empty MetrSpace; ::_thesis: for x being Element of X for S being sequence of X st S is_convergent_in_metrspace_to x holds lim S = x let x be Element of X; ::_thesis: for S being sequence of X st S is_convergent_in_metrspace_to x holds lim S = x let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x implies lim S = x ) assume S is_convergent_in_metrspace_to x ; ::_thesis: lim S = x then ( S is convergent & ( for r being Real st 0 < r holds ex m being Element of NAT st for n being Element of NAT st m <= n holds dist ((S . n),x) < r ) ) by Def2, Th9; hence lim S = x by TBSP_1:def_3; ::_thesis: verum end; theorem Th12: :: METRIC_6:12 for X being non empty MetrSpace for x being Element of X for S being sequence of X holds ( S is_convergent_in_metrspace_to x iff ( S is convergent & lim S = x ) ) proof let X be non empty MetrSpace; ::_thesis: for x being Element of X for S being sequence of X holds ( S is_convergent_in_metrspace_to x iff ( S is convergent & lim S = x ) ) let x be Element of X; ::_thesis: for S being sequence of X holds ( S is_convergent_in_metrspace_to x iff ( S is convergent & lim S = x ) ) let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x iff ( S is convergent & lim S = x ) ) ( S is convergent & lim S = x implies S is_convergent_in_metrspace_to x ) proof assume ( S is convergent & lim S = x ) ; ::_thesis: S is_convergent_in_metrspace_to x then for r being Real st 0 < r holds ex m being Element of NAT st for n being Element of NAT st m <= n holds dist ((S . n),x) < r by TBSP_1:def_3; hence S is_convergent_in_metrspace_to x by Def2; ::_thesis: verum end; hence ( S is_convergent_in_metrspace_to x iff ( S is convergent & lim S = x ) ) by Th9, Th11; ::_thesis: verum end; theorem Th13: :: METRIC_6:13 for X being non empty MetrSpace for S being sequence of X st S is convergent holds ex x being Element of X st ( S is_convergent_in_metrspace_to x & lim S = x ) proof let X be non empty MetrSpace; ::_thesis: for S being sequence of X st S is convergent holds ex x being Element of X st ( S is_convergent_in_metrspace_to x & lim S = x ) let S be sequence of X; ::_thesis: ( S is convergent implies ex x being Element of X st ( S is_convergent_in_metrspace_to x & lim S = x ) ) assume S is convergent ; ::_thesis: ex x being Element of X st ( S is_convergent_in_metrspace_to x & lim S = x ) then ex x being Element of X st S is_convergent_in_metrspace_to x by Th10; hence ex x being Element of X st ( S is_convergent_in_metrspace_to x & lim S = x ) by Th11; ::_thesis: verum end; theorem Th14: :: METRIC_6:14 for X being non empty MetrSpace for x being Element of X for S being sequence of X holds ( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) ) proof let X be non empty MetrSpace; ::_thesis: for x being Element of X for S being sequence of X holds ( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) ) let x be Element of X; ::_thesis: for S being sequence of X holds ( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) ) let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) ) A1: ( S is_convergent_in_metrspace_to x implies ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) ) proof assume A2: S is_convergent_in_metrspace_to x ; ::_thesis: ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) A3: for r being real number st 0 < r holds ex m being Element of NAT st for n being Element of NAT st m <= n holds abs (((dist_to_point (S,x)) . n) - 0) < r proof let r be real number ; ::_thesis: ( 0 < r implies ex m being Element of NAT st for n being Element of NAT st m <= n holds abs (((dist_to_point (S,x)) . n) - 0) < r ) assume A4: 0 < r ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds abs (((dist_to_point (S,x)) . n) - 0) < r reconsider r = r as Real by XREAL_0:def_1; consider m1 being Element of NAT such that A5: for n being Element of NAT st m1 <= n holds dist ((S . n),x) < r by A2, A4, Def2; take k = m1; ::_thesis: for n being Element of NAT st k <= n holds abs (((dist_to_point (S,x)) . n) - 0) < r let n be Element of NAT ; ::_thesis: ( k <= n implies abs (((dist_to_point (S,x)) . n) - 0) < r ) assume k <= n ; ::_thesis: abs (((dist_to_point (S,x)) . n) - 0) < r then dist ((S . n),x) < r by A5; then A6: (dist_to_point (S,x)) . n < r by Def6; dist ((S . n),x) = (dist_to_point (S,x)) . n by Def6; then 0 <= (dist_to_point (S,x)) . n by METRIC_1:5; hence abs (((dist_to_point (S,x)) . n) - 0) < r by A6, ABSVALUE:def_1; ::_thesis: verum end; then dist_to_point (S,x) is convergent by SEQ_2:def_6; hence ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) by A3, SEQ_2:def_7; ::_thesis: verum end; ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 implies S is_convergent_in_metrspace_to x ) proof assume A7: ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) ; ::_thesis: S is_convergent_in_metrspace_to x for r being Real st 0 < r holds ex m being Element of NAT st for n being Element of NAT st m <= n holds dist ((S . n),x) < r proof let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st for n being Element of NAT st m <= n holds dist ((S . n),x) < r ) assume 0 < r ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds dist ((S . n),x) < r then consider m1 being Element of NAT such that A8: for n being Element of NAT st m1 <= n holds abs (((dist_to_point (S,x)) . n) - 0) < r by A7, SEQ_2:def_7; take k = m1; ::_thesis: for n being Element of NAT st k <= n holds dist ((S . n),x) < r let n be Element of NAT ; ::_thesis: ( k <= n implies dist ((S . n),x) < r ) assume k <= n ; ::_thesis: dist ((S . n),x) < r then abs (((dist_to_point (S,x)) . n) - 0) < r by A8; then A9: abs (dist ((S . n),x)) < r by Def6; 0 <= dist ((S . n),x) by METRIC_1:5; hence dist ((S . n),x) < r by A9, ABSVALUE:def_1; ::_thesis: verum end; hence S is_convergent_in_metrspace_to x by Def2; ::_thesis: verum end; hence ( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) ) by A1; ::_thesis: verum end; theorem Th15: :: METRIC_6:15 for X being non empty MetrSpace for x being Element of X for S being sequence of X st S is_convergent_in_metrspace_to x holds for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S proof let X be non empty MetrSpace; ::_thesis: for x being Element of X for S being sequence of X st S is_convergent_in_metrspace_to x holds for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S let x be Element of X; ::_thesis: for S being sequence of X st S is_convergent_in_metrspace_to x holds for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x implies for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ) assume A1: S is_convergent_in_metrspace_to x ; ::_thesis: for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S thus for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ::_thesis: verum proof let r be Real; ::_thesis: ( 0 < r implies Ball (x,r) contains_almost_all_sequence S ) assume A2: 0 < r ; ::_thesis: Ball (x,r) contains_almost_all_sequence S ex m being Element of NAT st for n being Element of NAT st m <= n holds S . n in Ball (x,r) proof consider m1 being Element of NAT such that A3: for n being Element of NAT st m1 <= n holds dist ((S . n),x) < r by A1, A2, Def2; take k = m1; ::_thesis: for n being Element of NAT st k <= n holds S . n in Ball (x,r) now__::_thesis:_for_n_being_Element_of_NAT_st_k_<=_n_holds_ S_._n_in_Ball_(x,r) let n be Element of NAT ; ::_thesis: ( k <= n implies S . n in Ball (x,r) ) assume k <= n ; ::_thesis: S . n in Ball (x,r) then dist (x,(S . n)) < r by A3; hence S . n in Ball (x,r) by METRIC_1:11; ::_thesis: verum end; hence for n being Element of NAT st k <= n holds S . n in Ball (x,r) ; ::_thesis: verum end; hence Ball (x,r) contains_almost_all_sequence S by Def5; ::_thesis: verum end; end; theorem Th16: :: METRIC_6:16 for X being non empty MetrSpace for x being Element of X for S being sequence of X st ( for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ) holds for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S proof let X be non empty MetrSpace; ::_thesis: for x being Element of X for S being sequence of X st ( for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ) holds for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S let x be Element of X; ::_thesis: for S being sequence of X st ( for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ) holds for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S let S be sequence of X; ::_thesis: ( ( for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ) implies for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ) assume A1: for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ; ::_thesis: for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S A2: for r being Real st 0 < r holds ex m being Element of NAT st for n being Element of NAT st m <= n holds S . n in Ball (x,r) proof let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st for n being Element of NAT st m <= n holds S . n in Ball (x,r) ) assume 0 < r ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds S . n in Ball (x,r) then Ball (x,r) contains_almost_all_sequence S by A1; hence ex m being Element of NAT st for n being Element of NAT st m <= n holds S . n in Ball (x,r) by Def5; ::_thesis: verum end; thus for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ::_thesis: verum proof let V be Subset of X; ::_thesis: ( x in V & V in Family_open_set X implies V contains_almost_all_sequence S ) assume ( x in V & V in Family_open_set X ) ; ::_thesis: V contains_almost_all_sequence S then consider q being Real such that A3: 0 < q and A4: Ball (x,q) c= V by PCOMPS_1:def_4; consider m1 being Element of NAT such that A5: for n being Element of NAT st m1 <= n holds S . n in Ball (x,q) by A2, A3; now__::_thesis:_for_n_being_Element_of_NAT_st_m1_<=_n_holds_ S_._n_in_V let n be Element of NAT ; ::_thesis: ( m1 <= n implies S . n in V ) assume m1 <= n ; ::_thesis: S . n in V then S . n in Ball (x,q) by A5; hence S . n in V by A4; ::_thesis: verum end; hence V contains_almost_all_sequence S by Def5; ::_thesis: verum end; end; theorem Th17: :: METRIC_6:17 for X being non empty MetrSpace for x being Element of X for S being sequence of X st ( for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ) holds S is_convergent_in_metrspace_to x proof let X be non empty MetrSpace; ::_thesis: for x being Element of X for S being sequence of X st ( for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ) holds S is_convergent_in_metrspace_to x let x be Element of X; ::_thesis: for S being sequence of X st ( for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ) holds S is_convergent_in_metrspace_to x let S be sequence of X; ::_thesis: ( ( for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ) implies S is_convergent_in_metrspace_to x ) A1: for r being Real st 0 < r holds x in Ball (x,r) proof let r be Real; ::_thesis: ( 0 < r implies x in Ball (x,r) ) assume 0 < r ; ::_thesis: x in Ball (x,r) then dist (x,x) < r by METRIC_1:1; hence x in Ball (x,r) by METRIC_1:11; ::_thesis: verum end; assume A2: for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ; ::_thesis: S is_convergent_in_metrspace_to x for r being Real st 0 < r holds ex m being Element of NAT st for n being Element of NAT st m <= n holds dist ((S . n),x) < r proof let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st for n being Element of NAT st m <= n holds dist ((S . n),x) < r ) assume 0 < r ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds dist ((S . n),x) < r then x in Ball (x,r) by A1; then Ball (x,r) contains_almost_all_sequence S by A2, PCOMPS_1:29; then consider m1 being Element of NAT such that A3: for n being Element of NAT st m1 <= n holds S . n in Ball (x,r) by Def5; take k = m1; ::_thesis: for n being Element of NAT st k <= n holds dist ((S . n),x) < r let n be Element of NAT ; ::_thesis: ( k <= n implies dist ((S . n),x) < r ) assume k <= n ; ::_thesis: dist ((S . n),x) < r then S . n in Ball (x,r) by A3; hence dist ((S . n),x) < r by METRIC_1:11; ::_thesis: verum end; hence S is_convergent_in_metrspace_to x by Def2; ::_thesis: verum end; theorem :: METRIC_6:18 for X being non empty MetrSpace for x being Element of X for S being sequence of X holds ( S is_convergent_in_metrspace_to x iff for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ) proof let X be non empty MetrSpace; ::_thesis: for x being Element of X for S being sequence of X holds ( S is_convergent_in_metrspace_to x iff for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ) let x be Element of X; ::_thesis: for S being sequence of X holds ( S is_convergent_in_metrspace_to x iff for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ) let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x iff for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ) thus ( S is_convergent_in_metrspace_to x implies for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ) by Th15; ::_thesis: ( ( for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ) implies S is_convergent_in_metrspace_to x ) thus ( ( for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ) implies S is_convergent_in_metrspace_to x ) ::_thesis: verum proof assume for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ; ::_thesis: S is_convergent_in_metrspace_to x then for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S by Th16; hence S is_convergent_in_metrspace_to x by Th17; ::_thesis: verum end; end; theorem :: METRIC_6:19 for X being non empty MetrSpace for x being Element of X for S being sequence of X holds ( S is_convergent_in_metrspace_to x iff for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ) proof let X be non empty MetrSpace; ::_thesis: for x being Element of X for S being sequence of X holds ( S is_convergent_in_metrspace_to x iff for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ) let x be Element of X; ::_thesis: for S being sequence of X holds ( S is_convergent_in_metrspace_to x iff for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ) let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x iff for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ) thus ( S is_convergent_in_metrspace_to x implies for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ) ::_thesis: ( ( for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ) implies S is_convergent_in_metrspace_to x ) proof assume S is_convergent_in_metrspace_to x ; ::_thesis: for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S then for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S by Th15; hence for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S by Th16; ::_thesis: verum end; thus ( ( for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ) implies S is_convergent_in_metrspace_to x ) by Th17; ::_thesis: verum end; theorem :: METRIC_6:20 for X being non empty MetrSpace for x being Element of X for S being sequence of X holds ( ( for r being Real st 0 < r holds Ball (x,r) contains_almost_all_sequence S ) iff for V being Subset of X st x in V & V in Family_open_set X holds V contains_almost_all_sequence S ) by Th15, Th16, Th17; theorem Th21: :: METRIC_6:21 for X being non empty MetrSpace for S, T being sequence of X st S is convergent & T is convergent holds dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T)) proof let X be non empty MetrSpace; ::_thesis: for S, T being sequence of X st S is convergent & T is convergent holds dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T)) let S, T be sequence of X; ::_thesis: ( S is convergent & T is convergent implies dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T)) ) assume that A1: S is convergent and A2: T is convergent ; ::_thesis: dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T)) consider x being Element of X such that A3: S is_convergent_in_metrspace_to x and A4: lim S = x by A1, Th13; consider y being Element of X such that A5: T is_convergent_in_metrspace_to y and A6: lim T = y by A2, Th13; A7: for r being real number st 0 < r holds ex m being Element of NAT st for n being Element of NAT st m <= n holds abs (((sequence_of_dist (S,T)) . n) - (dist (x,y))) < r proof let r be real number ; ::_thesis: ( 0 < r implies ex m being Element of NAT st for n being Element of NAT st m <= n holds abs (((sequence_of_dist (S,T)) . n) - (dist (x,y))) < r ) assume A8: 0 < r ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds abs (((sequence_of_dist (S,T)) . n) - (dist (x,y))) < r reconsider r = r as Real by XREAL_0:def_1; A9: 0 < r / 2 by A8, XREAL_1:215; then consider m1 being Element of NAT such that A10: for n being Element of NAT st m1 <= n holds dist ((S . n),x) < r / 2 by A3, Def2; consider m2 being Element of NAT such that A11: for n being Element of NAT st m2 <= n holds dist ((T . n),y) < r / 2 by A5, A9, Def2; take k = m1 + m2; ::_thesis: for n being Element of NAT st k <= n holds abs (((sequence_of_dist (S,T)) . n) - (dist (x,y))) < r let n be Element of NAT ; ::_thesis: ( k <= n implies abs (((sequence_of_dist (S,T)) . n) - (dist (x,y))) < r ) assume A12: k <= n ; ::_thesis: abs (((sequence_of_dist (S,T)) . n) - (dist (x,y))) < r ( abs ((dist ((S . n),(T . n))) - (dist (x,(T . n)))) <= dist ((S . n),x) & abs ((dist ((T . n),x)) - (dist (y,x))) <= dist ((T . n),y) ) by Th1; then A13: (abs ((dist ((S . n),(T . n))) - (dist ((T . n),x)))) + (abs ((dist ((T . n),x)) - (dist (x,y)))) <= (dist ((S . n),x)) + (dist ((T . n),y)) by XREAL_1:7; abs (((sequence_of_dist (S,T)) . n) - (dist ((lim S),(lim T)))) = abs ((dist ((S . n),(T . n))) - (dist (x,y))) by A4, A6, Def7 .= abs (((dist ((S . n),(T . n))) - (dist ((T . n),x))) + ((dist ((T . n),x)) - (dist (x,y)))) ; then abs (((sequence_of_dist (S,T)) . n) - (dist ((lim S),(lim T)))) <= (abs ((dist ((S . n),(T . n))) - (dist ((T . n),x)))) + (abs ((dist ((T . n),x)) - (dist (x,y)))) by COMPLEX1:56; then A14: abs (((sequence_of_dist (S,T)) . n) - (dist ((lim S),(lim T)))) <= (dist ((S . n),x)) + (dist ((T . n),y)) by A13, XXREAL_0:2; m2 <= k by NAT_1:12; then m2 <= n by A12, XXREAL_0:2; then A15: dist ((T . n),y) < r / 2 by A11; m1 <= k by NAT_1:11; then m1 <= n by A12, XXREAL_0:2; then dist ((S . n),x) < r / 2 by A10; then (dist ((S . n),x)) + (dist ((T . n),y)) < (r / 2) + (r / 2) by A15, XREAL_1:8; hence abs (((sequence_of_dist (S,T)) . n) - (dist (x,y))) < r by A4, A6, A14, XXREAL_0:2; ::_thesis: verum end; then sequence_of_dist (S,T) is convergent by SEQ_2:def_6; hence dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T)) by A4, A6, A7, SEQ_2:def_7; ::_thesis: verum end; theorem :: METRIC_6:22 for X being non empty MetrSpace for x, y being Element of X for S being sequence of X st S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y holds x = y proof let X be non empty MetrSpace; ::_thesis: for x, y being Element of X for S being sequence of X st S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y holds x = y let x, y be Element of X; ::_thesis: for S being sequence of X st S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y holds x = y let S be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y implies x = y ) assume that A1: S is_convergent_in_metrspace_to x and A2: S is_convergent_in_metrspace_to y ; ::_thesis: x = y A3: lim S = y by A2, Th12; A4: for n being Nat holds (sequence_of_dist (S,S)) . n = 0 proof let n be Nat; ::_thesis: (sequence_of_dist (S,S)) . n = 0 n in NAT by ORDINAL1:def_12; then (sequence_of_dist (S,S)) . n = dist ((S . n),(S . n)) by Def7 .= 0 by METRIC_1:1 ; hence (sequence_of_dist (S,S)) . n = 0 ; ::_thesis: verum end; A5: ex n being Element of NAT st (sequence_of_dist (S,S)) . n = 0 proof take 0 ; ::_thesis: (sequence_of_dist (S,S)) . 0 = 0 thus (sequence_of_dist (S,S)) . 0 = 0 by A4; ::_thesis: verum end; ( lim S = x & S is convergent ) by A1, Th12; then A6: dist (x,y) = lim (sequence_of_dist (S,S)) by A3, Th21; sequence_of_dist (S,S) is constant by A4, VALUED_0:def_18; then dist (x,y) = 0 by A6, A5, SEQ_4:25; hence x = y by METRIC_1:2; ::_thesis: verum end; theorem Th23: :: METRIC_6:23 for X being non empty MetrSpace for S being sequence of X st S is constant holds S is convergent proof let X be non empty MetrSpace; ::_thesis: for S being sequence of X st S is constant holds S is convergent let S be sequence of X; ::_thesis: ( S is constant implies S is convergent ) assume S is constant ; ::_thesis: S is convergent then consider x being Element of X such that A1: for n being Nat holds S . n = x by VALUED_0:def_18; take x ; :: according to TBSP_1:def_2 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= dist ((S . b3),x) ) ) let r be Real; ::_thesis: ( r <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not r <= dist ((S . b2),x) ) ) assume A2: 0 < r ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not r <= dist ((S . b2),x) ) take k = 0 ; ::_thesis: for b1 being Element of NAT holds ( not k <= b1 or not r <= dist ((S . b1),x) ) now__::_thesis:_for_n_being_Element_of_NAT_st_k_<=_n_holds_ dist_((S_._n),x)_<_r let n be Element of NAT ; ::_thesis: ( k <= n implies dist ((S . n),x) < r ) assume k <= n ; ::_thesis: dist ((S . n),x) < r dist ((S . n),x) = dist (x,x) by A1 .= 0 by METRIC_1:1 ; hence dist ((S . n),x) < r by A2; ::_thesis: verum end; hence for n being Element of NAT st k <= n holds dist ((S . n),x) < r ; ::_thesis: verum end; theorem :: METRIC_6:24 for X being non empty MetrSpace for x being Element of X for S, S1 being sequence of X st S is_convergent_in_metrspace_to x & S1 is subsequence of S holds S1 is_convergent_in_metrspace_to x proof let X be non empty MetrSpace; ::_thesis: for x being Element of X for S, S1 being sequence of X st S is_convergent_in_metrspace_to x & S1 is subsequence of S holds S1 is_convergent_in_metrspace_to x let x be Element of X; ::_thesis: for S, S1 being sequence of X st S is_convergent_in_metrspace_to x & S1 is subsequence of S holds S1 is_convergent_in_metrspace_to x let S, S1 be sequence of X; ::_thesis: ( S is_convergent_in_metrspace_to x & S1 is subsequence of S implies S1 is_convergent_in_metrspace_to x ) assume that A1: S is_convergent_in_metrspace_to x and A2: S1 is subsequence of S ; ::_thesis: S1 is_convergent_in_metrspace_to x consider Nseq being increasing sequence of NAT such that A3: S1 = S * Nseq by A2, VALUED_0:def_17; for r being Real st 0 < r holds ex m being Element of NAT st for n being Element of NAT st m <= n holds dist ((S1 . n),x) < r proof let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st for n being Element of NAT st m <= n holds dist ((S1 . n),x) < r ) assume 0 < r ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds dist ((S1 . n),x) < r then consider m1 being Element of NAT such that A4: for n being Element of NAT st m1 <= n holds dist ((S . n),x) < r by A1, Def2; take m = m1; ::_thesis: for n being Element of NAT st m <= n holds dist ((S1 . n),x) < r for n being Element of NAT st m <= n holds dist ((S1 . n),x) < r proof let n be Element of NAT ; ::_thesis: ( m <= n implies dist ((S1 . n),x) < r ) assume A5: m <= n ; ::_thesis: dist ((S1 . n),x) < r dom S = NAT by FUNCT_2:def_1; then ( dom Nseq = NAT & Nseq . n in dom S ) by FUNCT_2:def_1; then n in dom (S * Nseq) by FUNCT_1:11; then A6: S1 . n = S . (Nseq . n) by A3, FUNCT_1:12; n <= Nseq . n by SEQM_3:14; then m1 <= Nseq . n by A5, XXREAL_0:2; hence dist ((S1 . n),x) < r by A4, A6; ::_thesis: verum end; hence for n being Element of NAT st m <= n holds dist ((S1 . n),x) < r ; ::_thesis: verum end; hence S1 is_convergent_in_metrspace_to x by Def2; ::_thesis: verum end; theorem :: METRIC_6:25 for X being non empty MetrSpace for S, S1 being sequence of X st S is Cauchy & S1 is subsequence of S holds S1 is Cauchy proof let X be non empty MetrSpace; ::_thesis: for S, S1 being sequence of X st S is Cauchy & S1 is subsequence of S holds S1 is Cauchy let S, S1 be sequence of X; ::_thesis: ( S is Cauchy & S1 is subsequence of S implies S1 is Cauchy ) assume that A1: S is Cauchy and A2: S1 is subsequence of S ; ::_thesis: S1 is Cauchy consider Nseq being increasing sequence of NAT such that A3: S1 = S * Nseq by A2, VALUED_0:def_17; for r being Real st 0 < r holds ex m being Element of NAT st for n, k being Element of NAT st m <= n & m <= k holds dist ((S1 . n),(S1 . k)) < r proof let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st for n, k being Element of NAT st m <= n & m <= k holds dist ((S1 . n),(S1 . k)) < r ) assume 0 < r ; ::_thesis: ex m being Element of NAT st for n, k being Element of NAT st m <= n & m <= k holds dist ((S1 . n),(S1 . k)) < r then consider m1 being Element of NAT such that A4: for n, k being Element of NAT st m1 <= n & m1 <= k holds dist ((S . n),(S . k)) < r by A1, TBSP_1:def_4; take m = m1; ::_thesis: for n, k being Element of NAT st m <= n & m <= k holds dist ((S1 . n),(S1 . k)) < r for n, k being Element of NAT st m <= n & m <= k holds dist ((S1 . n),(S1 . k)) < r proof let n, k be Element of NAT ; ::_thesis: ( m <= n & m <= k implies dist ((S1 . n),(S1 . k)) < r ) assume that A5: m <= n and A6: m <= k ; ::_thesis: dist ((S1 . n),(S1 . k)) < r k <= Nseq . k by SEQM_3:14; then A7: m1 <= Nseq . k by A6, XXREAL_0:2; dom S = NAT by FUNCT_2:def_1; then ( dom Nseq = NAT & Nseq . k in dom S ) by FUNCT_2:def_1; then k in dom (S * Nseq) by FUNCT_1:11; then A8: S1 . k = S . (Nseq . k) by A3, FUNCT_1:12; dom S = NAT by FUNCT_2:def_1; then ( dom Nseq = NAT & Nseq . n in dom S ) by FUNCT_2:def_1; then n in dom (S * Nseq) by FUNCT_1:11; then A9: S1 . n = S . (Nseq . n) by A3, FUNCT_1:12; n <= Nseq . n by SEQM_3:14; then m1 <= Nseq . n by A5, XXREAL_0:2; hence dist ((S1 . n),(S1 . k)) < r by A4, A9, A7, A8; ::_thesis: verum end; hence for n, k being Element of NAT st m <= n & m <= k holds dist ((S1 . n),(S1 . k)) < r ; ::_thesis: verum end; hence S1 is Cauchy by TBSP_1:def_4; ::_thesis: verum end; theorem :: METRIC_6:26 for X being non empty MetrSpace for S being sequence of X st S is constant holds S is Cauchy by Th23, TBSP_1:5; theorem :: METRIC_6:27 for X being non empty MetrSpace for S being sequence of X st S is convergent holds S is bounded proof let X be non empty MetrSpace; ::_thesis: for S being sequence of X st S is convergent holds S is bounded let S be sequence of X; ::_thesis: ( S is convergent implies S is bounded ) assume S is convergent ; ::_thesis: S is bounded then consider x being Element of X such that A1: S is_convergent_in_metrspace_to x and lim S = x by Th13; dist_to_point (S,x) is convergent by A1, Th14; then dist_to_point (S,x) is bounded by SEQ_2:13; then consider r being real number such that A2: 0 < r and A3: for n being Element of NAT holds abs ((dist_to_point (S,x)) . n) < r by SEQ_2:3; reconsider r = r as Real by XREAL_0:def_1; for n being Element of NAT holds S . n in Ball (x,r) proof let n be Element of NAT ; ::_thesis: S . n in Ball (x,r) A4: (dist_to_point (S,x)) . n = dist ((S . n),x) by Def6; then 0 <= (dist_to_point (S,x)) . n by METRIC_1:5; then abs ((dist_to_point (S,x)) . n) = (dist_to_point (S,x)) . n by ABSVALUE:def_1; then dist ((S . n),x) < r by A3, A4; hence S . n in Ball (x,r) by METRIC_1:11; ::_thesis: verum end; hence S is bounded by A2, Th8; ::_thesis: verum end; theorem Th28: :: METRIC_6:28 for X being non empty MetrSpace for S being sequence of X st S is Cauchy holds S is bounded proof let X be non empty MetrSpace; ::_thesis: for S being sequence of X st S is Cauchy holds S is bounded let S be sequence of X; ::_thesis: ( S is Cauchy implies S is bounded ) assume A1: S is Cauchy ; ::_thesis: S is bounded now__::_thesis:_ex_r_being_Element_of_NAT_st_ (_0_<_r_&_ex_m_being_Element_of_NAT_st_ for_n,_k_being_Element_of_NAT_st_m_<=_n_&_m_<=_k_holds_ dist_((S_._n),(S_._k))_<_r_) take r = 1; ::_thesis: ( 0 < r & ex m being Element of NAT st for n, k being Element of NAT st m <= n & m <= k holds dist ((S . n),(S . k)) < r ) thus 0 < r ; ::_thesis: ex m being Element of NAT st for n, k being Element of NAT st m <= n & m <= k holds dist ((S . n),(S . k)) < r consider m1 being Element of NAT such that A2: for n, k being Element of NAT st m1 <= n & m1 <= k holds dist ((S . n),(S . k)) < r by A1, TBSP_1:def_4; take m = m1; ::_thesis: for n, k being Element of NAT st m <= n & m <= k holds dist ((S . n),(S . k)) < r thus for n, k being Element of NAT st m <= n & m <= k holds dist ((S . n),(S . k)) < r by A2; ::_thesis: verum end; then consider r2 being Real, m1 being Element of NAT such that A3: 0 < r2 and A4: for n, k being Element of NAT st m1 <= n & m1 <= k holds dist ((S . n),(S . k)) < r2 ; consider r1 being real number such that A5: 0 < r1 and A6: for m2 being Element of NAT st m2 <= m1 holds abs ((dist_to_point (S,(S . m1))) . m2) < r1 by SEQ_2:4; A7: for m being Element of NAT st m <= m1 holds dist ((S . m),(S . m1)) < r1 proof let m be Element of NAT ; ::_thesis: ( m <= m1 implies dist ((S . m),(S . m1)) < r1 ) assume A8: m <= m1 ; ::_thesis: dist ((S . m),(S . m1)) < r1 A9: (dist_to_point (S,(S . m1))) . m = dist ((S . m),(S . m1)) by Def6; then 0 <= (dist_to_point (S,(S . m1))) . m by METRIC_1:5; then abs ((dist_to_point (S,(S . m1))) . m) = dist ((S . m),(S . m1)) by A9, ABSVALUE:def_1; hence dist ((S . m),(S . m1)) < r1 by A6, A8; ::_thesis: verum end; ex r being Real ex x being Element of X st ( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) proof reconsider r = r1 + r2 as Real ; take r ; ::_thesis: ex x being Element of X st ( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) take x = S . m1; ::_thesis: ( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) for n being Element of NAT holds S . n in Ball (x,r) proof let n be Element of NAT ; ::_thesis: S . n in Ball (x,r) now__::_thesis:_S_._n_in_Ball_(x,r) percases ( n <= m1 or m1 <= n ) ; supposeA10: n <= m1 ; ::_thesis: S . n in Ball (x,r) A11: r1 < r by A3, XREAL_1:29; dist ((S . n),(S . m1)) < r1 by A7, A10; then dist ((S . n),x) < r by A11, XXREAL_0:2; hence S . n in Ball (x,r) by METRIC_1:11; ::_thesis: verum end; supposeA12: m1 <= n ; ::_thesis: S . n in Ball (x,r) A13: r2 < r by A5, XREAL_1:29; dist ((S . n),(S . m1)) < r2 by A4, A12; then dist ((S . n),x) < r by A13, XXREAL_0:2; hence S . n in Ball (x,r) by METRIC_1:11; ::_thesis: verum end; end; end; hence S . n in Ball (x,r) ; ::_thesis: verum end; hence ( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) by A3, A5; ::_thesis: verum end; hence S is bounded by Th8; ::_thesis: verum end; registration let M be non empty MetrSpace; cluster Function-like constant V30( NAT , the carrier of M) -> convergent for Element of bool [:NAT, the carrier of M:]; coherence for b1 being sequence of M st b1 is constant holds b1 is convergent by Th23; cluster Function-like V30( NAT , the carrier of M) Cauchy -> bounded for Element of bool [:NAT, the carrier of M:]; coherence for b1 being sequence of M st b1 is Cauchy holds b1 is bounded by Th28; end; registration let M be non empty MetrSpace; cluster non empty Relation-like NAT -defined the carrier of M -valued Function-like constant V29( NAT ) V30( NAT , the carrier of M) convergent Cauchy bounded for Element of bool [:NAT, the carrier of M:]; existence ex b1 being sequence of M st ( b1 is constant & b1 is convergent & b1 is Cauchy & b1 is bounded ) proof set x = the Element of M; consider S being sequence of M such that A1: rng S = { the Element of M} by Th7; take S ; ::_thesis: ( S is constant & S is convergent & S is Cauchy & S is bounded ) thus A2: S is constant by A1, FUNCT_2:111; ::_thesis: ( S is convergent & S is Cauchy & S is bounded ) hence S is convergent ; ::_thesis: ( S is Cauchy & S is bounded ) thus S is Cauchy by A2; ::_thesis: S is bounded thus S is bounded by A2; ::_thesis: verum end; end; theorem :: METRIC_6:29 for X being non empty Reflexive symmetric triangle MetrStruct for V being bounded Subset of X for x being Element of X ex r being Real st ( 0 < r & V c= Ball (x,r) ) proof let X be non empty Reflexive symmetric triangle MetrStruct ; ::_thesis: for V being bounded Subset of X for x being Element of X ex r being Real st ( 0 < r & V c= Ball (x,r) ) let V be bounded Subset of X; ::_thesis: for x being Element of X ex r being Real st ( 0 < r & V c= Ball (x,r) ) let y be Element of X; ::_thesis: ex r being Real st ( 0 < r & V c= Ball (y,r) ) consider r being Real, x being Element of X such that A1: 0 < r and A2: V c= Ball (x,r) by Def3; take s = r + (dist (x,y)); ::_thesis: ( 0 < s & V c= Ball (y,s) ) dist (x,y) >= 0 by METRIC_1:5; then s >= r + 0 by XREAL_1:7; hence 0 < s by A1; ::_thesis: V c= Ball (y,s) let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in V or e in Ball (y,s) ) assume A3: e in V ; ::_thesis: e in Ball (y,s) then reconsider e = e as Element of X ; e in Ball (x,r) by A3, A2; then dist (e,x) < r by METRIC_1:11; then A4: (dist (e,x)) + (dist (x,y)) < r + (dist (x,y)) by XREAL_1:8; dist (e,y) <= (dist (e,x)) + (dist (x,y)) by METRIC_1:4; then dist (e,y) < r + (dist (x,y)) by A4, XXREAL_0:2; then e in Ball (y,s) by METRIC_1:11; hence e in Ball (y,s) ; ::_thesis: verum end;