let X be NormedLinearTopSpace; :: thesis: for V being Subset of X holds
( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )
let V be Subset of X; :: thesis: ( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )
consider RNS being RealNormSpace such that
A1: ( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) ) by Def7;
reconsider V1 = V as Subset of (TopSpaceNorm RNS) by A1;
hereby :: thesis: ( ( for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) ) implies V is open )
assume V is open ; :: thesis: for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V )
then A2: V1 is open by A1;
let x be Point of X; :: thesis: ( x in V implies ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )
reconsider x1 = x as Point of RNS by A1;
assume x in V ; :: thesis: ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V )
then consider r being Real such that
A3: ( r > 0 & { y where y is Point of RNS : ||.(x1 - y).|| < r } c= V1 ) by NORMSP_2:7, A2;
take r = r; :: thesis: ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V )
thus r > 0 by A3; :: thesis: { y where y is Point of X : ||.(x - y).|| < r } c= V
thus { y where y is Point of X : ||.(x - y).|| < r } c= V :: thesis: verum
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { y where y is Point of X : ||.(x - y).|| < r } or z in V )
assume z in { y where y is Point of X : ||.(x - y).|| < r } ; :: thesis: z in V
then consider y being Point of X such that
A4: ( y = z & ||.(x - y).|| < r ) ;
reconsider y1 = y as Point of RNS by A1;
||.(x1 - y1).|| < r by Th19, A1, A4;
then y1 in { y where y is Point of RNS : ||.(x1 - y).|| < r } ;
hence z in V by A4, A3; :: thesis: verum
end;
end;
assume A5: for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) ; :: thesis: V is open
now :: thesis: for x being Point of RNS st x in V1 holds
ex r being Real st
( r > 0 & { y where y is Point of RNS : ||.(x - y).|| < r } c= V1 )
let x be Point of RNS; :: thesis: ( x in V1 implies ex r being Real st
( r > 0 & { y where y is Point of RNS : ||.(x - y).|| < r } c= V1 ) )
reconsider x1 = x as Point of X by A1;
assume x in V1 ; :: thesis: ex r being Real st
( r > 0 & { y where y is Point of RNS : ||.(x - y).|| < r } c= V1 )
then consider r being Real such that
A6: ( r > 0 & { y where y is Point of X : ||.(x1 - y).|| < r } c= V ) by A5;
take r = r; :: thesis: ( r > 0 & { y where y is Point of RNS : ||.(x - y).|| < r } c= V1 )
thus r > 0 by A6; :: thesis: { y where y is Point of RNS : ||.(x - y).|| < r } c= V1
{ y where y is Point of RNS : ||.(x - y).|| < r } c= V1
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { y where y is Point of RNS : ||.(x - y).|| < r } or z in V1 )
assume z in { y where y is Point of RNS : ||.(x - y).|| < r } ; :: thesis: z in V1
then consider y being Point of RNS such that
A7: ( y = z & ||.(x - y).|| < r ) ;
reconsider y1 = y as Point of X by A1;
||.(x1 - y1).|| < r by Th19, A1, A7;
then y1 in { y where y is Point of X : ||.(x1 - y).|| < r } ;
hence z in V1 by A7, A6; :: thesis: verum
end;
hence { y where y is Point of RNS : ||.(x - y).|| < r } c= V1 ; :: thesis: verum
end;
then V1 is open by NORMSP_2:7;
hence V is open by A1; :: thesis: verum