let X be RealNormSpace; :: thesis: for Y being Subset of X
for v being VECTOR of X st Y is closed & ( for e being Real st 0 < e holds
ex w being VECTOR of X st
( w in Y & ||.(v - w).|| <= e ) ) holds
v in Y
let Y be Subset of X; :: thesis: for v being VECTOR of X st Y is closed & ( for e being Real st 0 < e holds
ex w being VECTOR of X st
( w in Y & ||.(v - w).|| <= e ) ) holds
v in Y
let v be VECTOR of X; :: thesis: ( Y is closed & ( for e being Real st 0 < e holds
ex w being VECTOR of X st
( w in Y & ||.(v - w).|| <= e ) ) implies v in Y )
assume that
A1: Y is closed and
A2: for e being Real st 0 < e holds
ex w being VECTOR of X st
( w in Y & ||.(v - w).|| <= e ) ; :: thesis: v in Y
assume A3: not v in Y ; :: thesis: contradiction
reconsider Z = Y ` as Subset of (TopSpaceNorm X) ;
A4: Z is open by A1, NORMSP_2:16;
v in the carrier of X \ Y by A3, XBOOLE_0:def 5;
then v in Z by SUBSET_1:def 4;
then consider e being Real such that
A5: ( e > 0 & { y where y is Point of X : ||.(v - y).|| < e } c= Z ) by A4, NORMSP_2:7;
consider w being VECTOR of X such that
A6: ( w in Y & ||.(v - w).|| <= e / 2 ) by A2, A5;
e / 2 < e by A5, XREAL_1:216;
then ||.(v - w).|| < e by A6, XXREAL_0:2;
then w in { y where y is Point of X : ||.(v - y).|| < e } ;
then w in Y ` by A5;
then w in the carrier of X \ Y by SUBSET_1:def 4;
hence contradiction by A6, XBOOLE_0:def 5; :: thesis: verum