let V be RealNormSpace; :: thesis: for x0 being Point of V st x0 <> 0. V holds
ex G being Point of (DualSp V) st
( (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / ||.x0.|| )
let x0 be Point of V; :: thesis: ( x0 <> 0. V implies ex G being Point of (DualSp V) st
( (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / ||.x0.|| ) )
assume AS0: x0 <> 0. V ; :: thesis: ex G being Point of (DualSp V) st
( (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / ||.x0.|| )
set X = NLin {(0. V)};
set Y = the carrier of (Lin {(0. V)});
for s being object holds
( s in the carrier of (Lin {(0. V)}) iff s in {(0. V)} )
proof
let s be object ; :: thesis: ( s in the carrier of (Lin {(0. V)}) iff s in {(0. V)} )
hereby :: thesis: ( s in {(0. V)} implies s in the carrier of (Lin {(0. V)}) )
assume s in the carrier of (Lin {(0. V)}) ; :: thesis: s in {(0. V)}
then s in Lin {(0. V)} ;
then ex a being Real st s = a * (0. V) by RLVECT_4:8;
hence s in {(0. V)} by TARSKI:def 1; :: thesis: verum
end;
assume s in {(0. V)} ; :: thesis: s in the carrier of (Lin {(0. V)})
then s = 1 * (0. V) by TARSKI:def 1;
then s in Lin {(0. V)} by RLVECT_4:8;
hence s in the carrier of (Lin {(0. V)}) ; :: thesis: verum
end;
then Y1: the carrier of (NLin {(0. V)}) = {(0. V)} by TARSKI:2;
set Z = { ||.(x - x0).|| where x is Point of V : x in NLin {(0. V)} } ;
Y2: for s being object holds
( s in { ||.(x - x0).|| where x is Point of V : x in NLin {(0. V)} } iff s in {||.x0.||} )
proof
let s be object ; :: thesis: ( s in { ||.(x - x0).|| where x is Point of V : x in NLin {(0. V)} } iff s in {||.x0.||} )
hereby :: thesis: ( s in {||.x0.||} implies s in { ||.(x - x0).|| where x is Point of V : x in NLin {(0. V)} } )
assume s in { ||.(x - x0).|| where x is Point of V : x in NLin {(0. V)} } ; :: thesis: s in {||.x0.||}
then consider x being Point of V such that
Y11: ( s = ||.(x - x0).|| & x in NLin {(0. V)} ) ;
x = 0. V by Y1, Y11, TARSKI:def 1;
then ||.(x - x0).|| = ||.x0.|| by NORMSP_1:2;
hence s in {||.x0.||} by TARSKI:def 1, Y11; :: thesis: verum
end;
assume s in {||.x0.||} ; :: thesis: s in { ||.(x - x0).|| where x is Point of V : x in NLin {(0. V)} }
then s = ||.x0.|| by TARSKI:def 1;
then X1: s = ||.((0. V) - x0).|| by NORMSP_1:2;
0. V in NLin {(0. V)} by Y1, TARSKI:def 1;
hence s in { ||.(x - x0).|| where x is Point of V : x in NLin {(0. V)} } by X1; :: thesis: verum
end;
then reconsider Z = { ||.(x - x0).|| where x is Point of V : x in NLin {(0. V)} } as non empty Subset of REAL by TARSKI:2;
reconsider d = lower_bound Z as Real ;
Y3: Z = {||.x0.||} by Y2;
then X4: d = ||.x0.|| by SEQ_4:9;
then d <> 0 by AS0, NORMSP_0:def 5;
then consider G being Point of (DualSp V) such that
X3: ( ( for x being Point of V st x in NLin {(0. V)} holds
(Bound2Lipschitz (G,V)) . x = 0 ) & (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / d ) by X4, Th63;
take G ; :: thesis: ( (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / ||.x0.|| )
thus ( (Bound2Lipschitz (G,V)) . x0 = 1 & ||.G.|| = 1 / ||.x0.|| ) by X3, SEQ_4:9, Y3; :: thesis: verum