:: 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-2011 Association of Mizar Users

begin

theorem :: NORMSP_2:1

for X being non empty MetrSpace
for Y being SetSequence of X st X is complete & union (rng Y) = the carrier of X & ( for n being Element of NAT holds (Y . n) ` in Family_open_set X ) holds
ex n0 being Element of NAT ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )

proof end;

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: :: NORMSP_2:def 1
for x, y being Point of X holds it . (x,y) = ||.(x - y).||;
existence
ex b₁ being Function of [: the carrier of X, the carrier of X:],REAL st
for x, y being Point of X holds b₁ . (x,y) = ||.(x - y).||

proof end;

uniqueness
for b₁, b₂ being Function of [: the carrier of X, the carrier of X:],REAL st ( for x, y being Point of X holds b₁ . (x,y) = ||.(x - y).|| ) & ( for x, y being Point of X holds b₂ . (x,y) = ||.(x - y).|| ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines distance_by_norm_of NORMSP_2:def 1 :
for X being RealNormSpace
for b₂ being Function of [: the carrier of X, the carrier of X:],REAL holds
( b₂ = distance_by_norm_of X iff for x, y being Point of X holds b₂ . (x,y) = ||.(x - y).|| );

Lm1: for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is Reflexive

proof end;

Lm2: for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is discerning

proof end;

Lm3: for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is symmetric

proof end;

Lm4: for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is triangle

proof end;

definition

let X be RealNormSpace;
func MetricSpaceNorm X -> non empty MetrSpace equals :: NORMSP_2:def 2
MetrStruct(# the carrier of X,(distance_by_norm_of X) #);
coherence
MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is non empty MetrSpace

proof end;

end;

:: deftheorem defines MetricSpaceNorm NORMSP_2:def 2 :
for X being RealNormSpace holds MetricSpaceNorm X = MetrStruct(# the carrier of X,(distance_by_norm_of X) #);

theorem Th2: :: NORMSP_2:2

for X being RealNormSpace
for z being Element of (MetricSpaceNorm X)
for r being real number ex x being Point of X st
( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } )

proof end;

theorem Th3: :: NORMSP_2:3

for X being RealNormSpace
for z being Element of (MetricSpaceNorm X)
for r being real number ex x being Point of X st
( x = z & cl_Ball (z,r) = { y where y is Point of X : ||.(x - y).|| <= r } )

proof end;

theorem Th4: :: NORMSP_2:4

for X being RealNormSpace
for S being sequence of X
for St being sequence of (MetricSpaceNorm X)
for x being Point of X
for xt being Point of (MetricSpaceNorm X) st S = St & x = xt holds
( St is_convergent_in_metrspace_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )

proof end;

theorem Th5: :: NORMSP_2:5

for X being RealNormSpace
for S being sequence of X
for St being sequence of (MetricSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )

proof end;

theorem Th6: :: NORMSP_2:6

for X being RealNormSpace
for S being sequence of X
for St being sequence of (MetricSpaceNorm X) st S = St & St is convergent holds
lim St = lim S

proof end;

begin

definition

let X be RealNormSpace;
func TopSpaceNorm X -> non empty TopSpace equals :: NORMSP_2:def 3
TopSpaceMetr (MetricSpaceNorm X);
coherence
TopSpaceMetr (MetricSpaceNorm X) is non empty TopSpace ;

end;

:: deftheorem defines TopSpaceNorm NORMSP_2:def 3 :
for X being RealNormSpace holds TopSpaceNorm X = TopSpaceMetr (MetricSpaceNorm X);

theorem Th7: :: NORMSP_2:7

for X being RealNormSpace
for V being Subset of (TopSpaceNorm X) holds
( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )

proof end;

theorem Th8: :: NORMSP_2:8

for X being RealNormSpace
for x being Point of X
for r being Real holds { y where y is Point of X : ||.(x - y).|| < r } is open Subset of (TopSpaceNorm X)

proof end;

theorem :: NORMSP_2:9

for X being RealNormSpace
for x being Point of X
for r being Real holds { y where y is Point of X : ||.(x - y).|| <= r } is closed Subset of (TopSpaceNorm X)

proof end;

theorem :: NORMSP_2:10

for X being non empty Hausdorff TopSpace st X is locally-compact holds
X is Baire

proof end;

theorem :: NORMSP_2:11

for X being RealNormSpace holds TopSpaceNorm X is sequential ;

registration

let X be RealNormSpace;
cluster TopSpaceNorm X -> non empty sequential ;
coherence
TopSpaceNorm X is sequential ;

end;

theorem Th12: :: NORMSP_2:12

for X being RealNormSpace
for S being sequence of X
for St being sequence of (TopSpaceNorm X)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )

proof end;

theorem Th13: :: NORMSP_2:13

for X being RealNormSpace
for S being sequence of X
for St being sequence of (TopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )

proof end;

theorem Th14: :: NORMSP_2:14

for X being RealNormSpace
for S being sequence of X
for St being sequence of (TopSpaceNorm X) st S = St & St is convergent holds
( Lim St = {(lim S)} & lim St = lim S )

proof end;

theorem Th15: :: NORMSP_2:15

for X being RealNormSpace
for V being Subset of X
for Vt being Subset of (TopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )

proof end;

theorem Th16: :: NORMSP_2:16

for X being RealNormSpace
for V being Subset of X
for Vt being Subset of (TopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )

proof end;

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 }

proof end;

theorem Th17: :: NORMSP_2:17

for X being RealNormSpace
for U being Subset of X
for Ut being Subset of (TopSpaceNorm X)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st U = Ut & x = xt holds
( U is Neighbourhood of x iff Ut is a_neighborhood of xt )

proof end;

theorem Th18: :: NORMSP_2:18

for X, Y being RealNormSpace
for f being PartFunc of X,Y
for ft being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_in x iff ft is_continuous_at xt )

proof end;

theorem :: NORMSP_2:19

for X, Y being RealNormSpace
for f being PartFunc of X,Y
for ft being Function of (TopSpaceNorm X),(TopSpaceNorm Y) st f = ft holds
( f is_continuous_on the carrier of X iff ft is continuous )

proof end;

begin

definition

let X be RealNormSpace;
func LinearTopSpaceNorm X -> non empty strict RLTopStruct means :Def4: :: NORMSP_2:def 4
( the carrier of it = the carrier of X & 0. it = 0. X & the addF of it = the addF of X & the Mult of it = the Mult of X & the topology of it = the topology of (TopSpaceNorm X) );
existence
ex b₁ being non empty strict RLTopStruct st
( the carrier of b₁ = the carrier of X & 0. b₁ = 0. X & the addF of b₁ = the addF of X & the Mult of b₁ = the Mult of X & the topology of b₁ = the topology of (TopSpaceNorm X) )

proof end;

uniqueness
for b₁, b₂ being non empty strict RLTopStruct st the carrier of b₁ = the carrier of X & 0. b₁ = 0. X & the addF of b₁ = the addF of X & the Mult of b₁ = the Mult of X & the topology of b₁ = the topology of (TopSpaceNorm X) & the carrier of b₂ = the carrier of X & 0. b₂ = 0. X & the addF of b₂ = the addF of X & the Mult of b₂ = the Mult of X & the topology of b₂ = the topology of (TopSpaceNorm X) holds
b₁ = b₂ ;

end;

:: deftheorem Def4 defines LinearTopSpaceNorm NORMSP_2:def 4 :
for X being RealNormSpace
for b₂ being non empty strict RLTopStruct holds
( b₂ = LinearTopSpaceNorm X iff ( the carrier of b₂ = the carrier of X & 0. b₂ = 0. X & the addF of b₂ = the addF of X & the Mult of b₂ = the Mult of X & the topology of b₂ = the topology of (TopSpaceNorm X) ) );

registration

let X be RealNormSpace;
cluster LinearTopSpaceNorm X -> non empty TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous ;
correctness
coherence
( LinearTopSpaceNorm X is add-continuous & LinearTopSpaceNorm X is Mult-continuous & LinearTopSpaceNorm X is TopSpace-like & LinearTopSpaceNorm X is Abelian & LinearTopSpaceNorm X is add-associative & LinearTopSpaceNorm X is right_zeroed & LinearTopSpaceNorm X is right_complementable & LinearTopSpaceNorm X is vector-distributive & LinearTopSpaceNorm X is scalar-distributive & LinearTopSpaceNorm X is scalar-associative & LinearTopSpaceNorm X is scalar-unital );

proof end;

end;

theorem Th20: :: NORMSP_2:20

for X being RealNormSpace
for V being Subset of (TopSpaceNorm X)
for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )

proof end;

theorem Th21: :: NORMSP_2:21

for X being RealNormSpace
for V being Subset of (TopSpaceNorm X)
for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )

proof end;

theorem :: NORMSP_2:22

for X being RealNormSpace
for V being Subset of (LinearTopSpaceNorm X) holds
( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )

proof end;

theorem :: NORMSP_2:23

for X being RealNormSpace
for x being Point of X
for r being Real
for V being Subset of (LinearTopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| < r } holds
V is open

proof end;

theorem :: NORMSP_2:24

for X being RealNormSpace
for x being Point of X
for r being Real
for V being Subset of (TopSpaceNorm X) st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed

proof end;

registration

let X be RealNormSpace;
cluster LinearTopSpaceNorm X -> non empty T_2 strict ;
coherence
LinearTopSpaceNorm X is T_2

proof end;

cluster LinearTopSpaceNorm X -> non empty sober strict ;
coherence
LinearTopSpaceNorm X is sober by YELLOW_8:31;

end;

theorem Th25: :: NORMSP_2:25

for X being RealNormSpace
for S being Subset-Family of (TopSpaceNorm X)
for St being Subset-Family of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is Basis of iff S is Basis of )

proof end;

registration

let X be RealNormSpace;
cluster LinearTopSpaceNorm X -> non empty first-countable strict ;
coherence
LinearTopSpaceNorm X is first-countable

proof end;

cluster LinearTopSpaceNorm X -> non empty Frechet strict ;
coherence
LinearTopSpaceNorm X is Frechet ;
cluster LinearTopSpaceNorm X -> non empty sequential strict ;
coherence
LinearTopSpaceNorm X is sequential ;

end;

theorem Th26: :: NORMSP_2:26

for X being RealNormSpace
for S being sequence of (TopSpaceNorm X)
for St being sequence of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )

proof end;

theorem Th27: :: NORMSP_2:27

for X being RealNormSpace
for S being sequence of (TopSpaceNorm X)
for St being sequence of (LinearTopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )

proof end;

theorem Th28: :: NORMSP_2:28

for X being RealNormSpace
for S being sequence of (TopSpaceNorm X)
for St being sequence of (LinearTopSpaceNorm X) st S = St & St is convergent holds
( Lim S = Lim St & lim S = lim St )

proof end;

theorem :: NORMSP_2:29

for X being RealNormSpace
for S being sequence of X
for St being sequence of (LinearTopSpaceNorm X)
for x being Point of X
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r )

proof end;

theorem :: NORMSP_2:30

for X being RealNormSpace
for S being sequence of X
for St being sequence of (LinearTopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )

proof end;

theorem :: NORMSP_2:31

for X being RealNormSpace
for S being sequence of X
for St being sequence of (LinearTopSpaceNorm X) st S = St & St is convergent holds
( Lim St = {(lim S)} & lim St = lim S )

proof end;

theorem :: NORMSP_2:32

for X being RealNormSpace
for V being Subset of X
for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )

proof end;

theorem :: NORMSP_2:33

for X being RealNormSpace
for V being Subset of X
for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )

proof end;

theorem Th34: :: NORMSP_2:34

for X being RealNormSpace
for U being Subset of (TopSpaceNorm X)
for Ut being Subset of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st U = Ut & x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )

proof end;

theorem Th35: :: NORMSP_2:35

for X, Y being RealNormSpace
for f being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for ft being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )

proof end;

theorem :: NORMSP_2:36

for X, Y being RealNormSpace
for f being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for ft being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) st f = ft holds
( f is continuous iff ft is continuous )

proof end;