begin
theorem
begin
definition
let X be
RealNormSpace;
func distance_by_norm_of X -> Function of
[:the carrier of X,the carrier of X:],
REAL means :
Def1:
for
x,
y being
Point of holds
it . x,
y = ||.(x - y).||;
existence
ex b1 being Function of [:the carrier of X,the carrier of X:], REAL st
for x, y being Point of holds b1 . x,y = ||.(x - y).||
uniqueness
for b1, b2 being Function of [:the carrier of X,the carrier of X:], REAL st ( for x, y being Point of holds b1 . x,y = ||.(x - y).|| ) & ( for x, y being Point of holds b2 . x,y = ||.(x - y).|| ) holds
b1 = b2
end;
:: deftheorem Def1 defines distance_by_norm_of NORMSP_2:def 1 :
Lm1:
for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is Reflexive
Lm2:
for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is discerning
Lm3:
for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is symmetric
Lm4:
for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is triangle
:: deftheorem defines MetricSpaceNorm NORMSP_2:def 2 :
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
begin
:: deftheorem defines TopSpaceNorm NORMSP_2:def 3 :
theorem Th7:
theorem Th8:
theorem
theorem
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
Lm5:
for X being RealNormSpace
for r being Real
for x being Point of holds { y where y is Point of : ||.(x - y).|| < r } = { y where y is Point of : ||.(y - x).|| < r }
theorem Th17:
theorem Th18:
theorem
begin
:: deftheorem Def4 defines LinearTopSpaceNorm NORMSP_2:def 4 :
theorem Th20:
theorem Th21:
theorem
theorem
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem
theorem
theorem
theorem
theorem
theorem Th34:
theorem Th35:
theorem