:: Baire's Category Theorem and Some Spaces Generated from Real Normed Space
:: by Noboru Endou , Yasunari Shidama and Katsumasa Okamura
::
:: Received November 21, 2006
:: Copyright (c) 2006 Association of Mizar Users
theorem :: NORMSP_2:1
definition
let X be
RealNormSpace;
func distance_by_norm_of X -> Function of
[:the carrier of X,the carrier of X:],
REAL means :
Def1:
:: NORMSP_2:def 1
for
x,
y being
Point of
X 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 X 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 X holds b1 . x,y = ||.(x - y).|| ) & ( for x, y being Point of X 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: :: NORMSP_2:2
theorem Th3: :: NORMSP_2:3
theorem Th4: :: NORMSP_2:4
theorem Th5: :: NORMSP_2:5
theorem Th6: :: NORMSP_2:6
:: deftheorem defines TopSpaceNorm NORMSP_2:def 3 :
theorem Th7: :: NORMSP_2:7
theorem Th8: :: NORMSP_2:8
theorem :: NORMSP_2:9
theorem :: NORMSP_2:10
theorem :: NORMSP_2:11
theorem Th12: :: NORMSP_2:12
theorem Th13: :: NORMSP_2:13
theorem Th14: :: NORMSP_2:14
theorem Th15: :: NORMSP_2:15
theorem Th16: :: NORMSP_2:16
Lm5:
for X being RealNormSpace
for r being Real
for x being Point of X holds { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r }
theorem Th17: :: NORMSP_2:17
theorem Th18: :: NORMSP_2:18
theorem :: NORMSP_2:19
:: deftheorem Def4 defines LinearTopSpaceNorm NORMSP_2:def 4 :
theorem Th20: :: NORMSP_2:20
theorem Th21: :: NORMSP_2:21
theorem :: NORMSP_2:22
theorem :: NORMSP_2:23
theorem :: NORMSP_2:24
theorem Th25: :: NORMSP_2:25
theorem Th26: :: NORMSP_2:26
theorem Th27: :: NORMSP_2:27
theorem Th28: :: NORMSP_2:28
theorem :: NORMSP_2:29
theorem :: NORMSP_2:30
theorem :: NORMSP_2:31
theorem :: NORMSP_2:32
theorem :: NORMSP_2:33
theorem Th34: :: NORMSP_2:34
theorem Th35: :: NORMSP_2:35
theorem :: NORMSP_2:36