let V be RealNormSpace; :: thesis: for Y being non empty Subset of V
for x0 being Point of V st Y is linearly-closed & Y is closed & not x0 in Y holds
ex G being Point of (DualSp V) st
( ( for x being Point of V st x in Y holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 )
let Y be non empty Subset of V; :: thesis: for x0 being Point of V st Y is linearly-closed & Y is closed & not x0 in Y holds
ex G being Point of (DualSp V) st
( ( for x being Point of V st x in Y holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 )
let x0 be Point of V; :: thesis: ( Y is linearly-closed & Y is closed & not x0 in Y implies ex G being Point of (DualSp V) st
( ( for x being Point of V st x in Y holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 ) )
assume AS: ( Y is linearly-closed & Y is closed & not x0 in Y ) ; :: thesis: ex G being Point of (DualSp V) st
( ( for x being Point of V st x in Y holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 )
set X = NLin Y;
X1: the carrier of (NLin Y) = Y by NORMSP_3:31, AS;
set Z = { ||.(x - x0).|| where x is Point of V : x in NLin Y } ;
NLin Y is Subspace of V by NORMSP_3:27;
then 0. V in NLin Y by RLSUB_1:17;
then X2: ||.((0. V) - x0).|| in { ||.(x - x0).|| where x is Point of V : x in NLin Y } ;
now :: thesis: for z being object st z in { ||.(x - x0).|| where x is Point of V : x in NLin Y } holds
z in REAL
let z be object ; :: thesis: ( z in { ||.(x - x0).|| where x is Point of V : x in NLin Y } implies z in REAL )
assume z in { ||.(x - x0).|| where x is Point of V : x in NLin Y } ; :: thesis: z in REAL
then ex x being Point of V st
( z = ||.(x - x0).|| & x in NLin Y ) ;
hence z in REAL ; :: thesis: verum
end;
then { ||.(x - x0).|| where x is Point of V : x in NLin Y } c= REAL ;
then reconsider Z = { ||.(x - x0).|| where x is Point of V : x in NLin Y } as non empty Subset of REAL by X2;
reconsider r0 = 0 as Real ;
for r being ExtReal st r in Z holds
r0 <= r
proof
let r be ExtReal; :: thesis: ( r in Z implies r0 <= r )
assume r in Z ; :: thesis: r0 <= r
then ex x being Point of V st
( r = ||.(x - x0).|| & x in NLin Y ) ;
hence r0 <= r ; :: thesis: verum
end;
then U1: r0 is LowerBound of Z by XXREAL_2:def 2;
then Z is bounded_below ;
then reconsider Z = Z as non empty real-membered bounded_below Subset of REAL ;
reconsider d = lower_bound Z as Real ;
X3: r0 <= inf Z by U1, XXREAL_2:def 4;
d > 0
proof
assume not d > 0 ; :: thesis: contradiction
then X22: d = 0 by X3;
reconsider Yt = Y ` as Subset of (TopSpaceNorm V) ;
Z24: Yt is open by AS, NORMSP_2:16;
x0 in the carrier of V \ Y by AS, XBOOLE_0:def 5;
then x0 in Yt by SUBSET_1:def 4;
then consider s being Real such that
X23: ( 0 < s & { y where y is Point of V : ||.(x0 - y).|| < s } c= Yt ) by Z24, NORMSP_2:7;
consider r being Real such that
X24: ( r in Z & r < 0 + s ) by X22, X23, SEQ_4:def 2;
consider x being Point of V such that
X25: ( r = ||.(x - x0).|| & x in NLin Y ) by X24;
||.(x0 - x).|| < s by X24, X25, NORMSP_1:7;
then x in { x where x is Point of V : ||.(x0 - x).|| < s } ;
then x in Yt by X23;
then x in the carrier of V \ Y by SUBSET_1:def 4;
hence contradiction by X1, X25, XBOOLE_0:def 5; :: thesis: verum
end;
then consider G being Point of (DualSp V) such that
X3: ( ( for x being Point of V st x in NLin Y holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / d ) by Th63;
take G ; :: thesis: ( ( for x being Point of V st x in Y holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 )
now :: thesis: for x being Point of V st x in Y holds
(Bound2Lipschitz (G,V)) . x = 0
let x be Point of V; :: thesis: ( x in Y implies (Bound2Lipschitz (G,V)) . x = 0 )
assume x in Y ; :: thesis: (Bound2Lipschitz (G,V)) . x = 0
then x in NLin Y by NORMSP_3:31, AS;
hence (Bound2Lipschitz (G,V)) . x = 0 by X3; :: thesis: verum
end;
hence ( ( for x being Point of V st x in Y holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 ) by X3; :: thesis: verum