let X be LinearTopSpace; :: thesis: for U being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st
( W is circled & W c= U )
let U be a_neighborhood of 0. X; :: thesis: ex W being a_neighborhood of 0. X st
( W is circled & W c= U )
0. X = 0 * (0. X) ;
then consider r being positive Real, V being a_neighborhood of 0. X such that
A1: for s being Real st |.(s - 0).| < r holds
s * V c= U by Th32;
set F = { (a * V) where a is Real : |.a.| < r } ;
{ (a * V) where a is Real : |.a.| < r } c= bool the carrier of X
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in { (a * V) where a is Real : |.a.| < r } or A in bool the carrier of X )
assume A in { (a * V) where a is Real : |.a.| < r } ; :: thesis: A in bool the carrier of X
then ex a being Real st
( A = a * V & |.a.| < r ) ;
hence A in bool the carrier of X ; :: thesis: verum
end;
then reconsider F = { (a * V) where a is Real : |.a.| < r } as Subset-Family of X ;
take union F ; :: thesis: ( union F is a_neighborhood of 0. X & union F is circled & union F c= U )
now :: thesis: for s being Real st |.s.| < r holds
s * V c= U
let s be Real; :: thesis: ( |.s.| < r implies s * V c= U )
assume |.s.| < r ; :: thesis: s * V c= U
then |.(s - 0).| < r ;
hence s * V c= U by A1; :: thesis: verum
end;
hence ( union F is a_neighborhood of 0. X & union F is circled & union F c= U ) by Lm20; :: thesis: verum