let X be RealNormSpace; :: thesis: for x being Point of X
for r being Real
for V being Subset of (TopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed
let x be Point of X; :: thesis: for r being Real
for V being Subset of (TopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed
let r be Real; :: thesis: for V being Subset of (TopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed
let V be Subset of (TopSpaceNorm X); :: thesis: ( V = { y where y is Point of X : ||.(x - y).|| <= r } implies V is closed )
assume A1: V = { y where y is Point of X : ||.(x - y).|| <= r } ; :: thesis: V is closed
reconsider z = x as Element of (MetricSpaceNorm X) ;
ex t being Point of X st
( t = x & cl_Ball (z,r) = { y where y is Point of X : ||.(t - y).|| <= r } ) by Th3;
hence V is closed by A1, TOPREAL6:57; :: thesis: verum