let V be RealNormSpace; :: thesis: for W being Subspace of V
for v being VECTOR of V holds NormVSets (V,W,v) is bounded_below
let W be Subspace of V; :: thesis: for v being VECTOR of V holds NormVSets (V,W,v) is bounded_below
let v be VECTOR of V; :: thesis: NormVSets (V,W,v) is bounded_below
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 NormVSets (V,W,v) is bounded_below by XXREAL_2:def 9; :: thesis: verum