let X be RealBanachSpace; :: thesis: for Y being SetSequence of X st union (rng Y) = the carrier of X & ( for n being Nat holds Y . n is closed ) holds
ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
let Y be SetSequence of X; :: thesis: ( union (rng Y) = the carrier of X & ( for n being Nat holds Y . n is closed ) implies ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 ) )
assume that
A1: union (rng Y) = the carrier of X and
A2: for n being Nat holds Y . n is closed ; :: thesis: ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
now :: thesis: for n being Nat holds (Y . n) ` in Family_open_set (MetricSpaceNorm X)
let n be Nat; :: thesis: (Y . n) ` in Family_open_set (MetricSpaceNorm X)
reconsider Yn = Y . n as Subset of (TopSpaceNorm X) ;
Y . n is closed by A2;
then Yn is closed by NORMSP_2:15;
then Yn ` is open by TOPS_1:3;
hence (Y . n) ` in Family_open_set (MetricSpaceNorm X) by PRE_TOPC:def 2; :: thesis: verum
end;
then consider n0 being Nat, r being Real, xx0 being Point of (MetricSpaceNorm X) such that
A3: ( 0 < r & Ball (xx0,r) c= Y . n0 ) by A1, NORMSP_2:1;
consider x0 being Point of X such that
x0 = xx0 and
A4: Ball (xx0,r) = { x where x is Point of X : ||.(x0 - x).|| < r } by NORMSP_2:2;
Ball (x0,r) = { x where x is Point of X : ||.(x0 - x).|| < r } ;
hence ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 ) by A3, A4; :: thesis: verum