:: deftheorem DeNorm defines NormCoset NORMSP_3:def 18 :
for V being RealNormSpace
for W being Subspace of V
for b₃ being Function of (CosetSet (V,W)),REAL holds
( b₃ = NormCoset (V,W) iff for A being Element of CosetSet (V,W)
for v being VECTOR of V st A = v + W holds
b₃ . A = lower_bound (NormVSets (V,W,v)) );