let V be RealNormSpace; :: thesis: for W being Subspace of V
for v being VECTOR of V holds
( 0 <= lower_bound (NormVSets (V,W,v)) & lower_bound (NormVSets (V,W,v)) <= ||.v.|| )
let W be Subspace of V; :: thesis: for v being VECTOR of V holds
( 0 <= lower_bound (NormVSets (V,W,v)) & lower_bound (NormVSets (V,W,v)) <= ||.v.|| )
let v be VECTOR of V; :: thesis: ( 0 <= lower_bound (NormVSets (V,W,v)) & lower_bound (NormVSets (V,W,v)) <= ||.v.|| )
for r being ExtReal st r in NormVSets (V,W,v) holds
0 <= r
proof
let r be ExtReal; :: thesis: ( r in NormVSets (V,W,v) implies 0 <= r )
assume r in NormVSets (V,W,v) ; :: thesis: 0 <= r
then consider x being VECTOR of V such that
A1: ( r = ||.x.|| & x in v + W ) ;
thus 0 <= r by A1; :: thesis: verum
end;
then 0 is LowerBound of NormVSets (V,W,v) by XXREAL_2:def 2;
hence 0 <= lower_bound (NormVSets (V,W,v)) by XXREAL_2:def 4; :: thesis: lower_bound (NormVSets (V,W,v)) <= ||.v.||
v in v + W by RLSUB_1:43;
then A2: ||.v.|| in NormVSets (V,W,v) ;
inf (NormVSets (V,W,v)) is LowerBound of NormVSets (V,W,v) by XXREAL_2:def 4;
hence lower_bound (NormVSets (V,W,v)) <= ||.v.|| by A2, XXREAL_2:def 2; :: thesis: verum