let X be NormedLinearTopSpace; :: thesis: for x being Point of X
for r being Real
for V being Subset of X st V = { y where y is Point of X : ||.(x - y).|| < r } holds
V is open
let x be Point of X; :: thesis: for r being Real
for V being Subset of X st V = { y where y is Point of X : ||.(x - y).|| < r } holds
V is open
let r be Real; :: thesis: for V being Subset of X st V = { y where y is Point of X : ||.(x - y).|| < r } holds
V is open
let V be Subset of X; :: thesis: ( V = { y where y is Point of X : ||.(x - y).|| < r } implies V is open )
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 V0 = V as Subset of (TopSpaceNorm RNS) by A1;
reconsider x1 = x as Point of RNS by A1;
assume A2: V = { y where y is Point of X : ||.(x - y).|| < r } ; :: thesis: V is open
for z being object holds
( z in { y where y is Point of X : ||.(x - y).|| < r } iff z in { y where y is Point of RNS : ||.(x1 - y).|| < r } )
proof
let z be object ; :: thesis: ( z in { y where y is Point of X : ||.(x - y).|| < r } iff z in { y where y is Point of RNS : ||.(x1 - y).|| < r } )
hereby :: thesis: ( z in { y where y is Point of RNS : ||.(x1 - y).|| < r } implies z in { y where y is Point of X : ||.(x - y).|| < r } )
assume z in { y where y is Point of X : ||.(x - y).|| < r } ; :: thesis: z in { y where y is Point of RNS : ||.(x1 - y).|| < r }
then consider y being Point of X such that
A3: ( y = z & ||.(x - y).|| < r ) ;
reconsider y1 = y as Point of RNS by A1;
||.(x1 - y1).|| < r by Th19, A1, A3;
hence z in { y where y is Point of RNS : ||.(x1 - y).|| < r } by A3; :: thesis: verum
end;
assume z in { y where y is Point of RNS : ||.(x1 - y).|| < r } ; :: thesis: z in { y where y is Point of X : ||.(x - y).|| < r }
then consider y1 being Point of RNS such that
A4: ( y1 = z & ||.(x1 - y1).|| < r ) ;
reconsider y = y1 as Point of X by A1;
||.(x - y).|| < r by Th19, A1, A4;
hence z in { y where y is Point of X : ||.(x - y).|| < r } by A4; :: thesis: verum
end;
then { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of RNS : ||.(x1 - y).|| < r } by TARSKI:2;
then V0 is open by NORMSP_2:8, A2;
hence V is open by A1; :: thesis: verum