:: 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-2012 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 &amp; Ball (x0,r) c= Y . n0 )
proofend;

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 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).||
proofend;
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).|| ) &amp; ( for x, y being Point of X holds b2 . (x,y) = ||.(x - y).|| ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines distance_by_norm_of NORMSP_2:def_1_:_
 for X being RealNormSpace
for b2 being Function of [: the carrier of X, the carrier of X:],REAL holds
( b2 = distance_by_norm_of X iff for x, y being Point of X holds b2 . (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
proofend;

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

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

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

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
proofend;
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 &amp; Ball (z,r) =  {  y where y is Point of X : ||.(x - y).|| < r  }  )
proofend;

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 &amp; cl_Ball (z,r) =  {  y where y is Point of X : ||.(x - y).|| <= r  }  )
proofend;

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 &amp; 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 )
proofend;

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 )
proofend;

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 &amp; St is convergent holds
lim St = lim S
proofend;

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 &amp;  {  y where y is Point of X : ||.(x - y).|| < r  }  c= V ) )
proofend;

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)
proofend;

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)
proofend;

:: [WP: ] Baire_Category_Theorem_(Hausdorff_spaces)
theorem :: NORMSP_2:10
for X being non empty Hausdorff TopSpace st X is locally-compact holds
X is Baire
proofend;

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 &amp; 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 )
proofend;

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 )
proofend;

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 &amp; St is convergent holds
( Lim St = {(lim S)} &amp; lim St = lim S )
proofend;

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 )
proofend;

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 )
proofend;

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  }
proofend;

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 &amp; x = xt holds
( U is Neighbourhood of x iff Ut is a_neighborhood of xt )
proofend;

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 &amp; x = xt holds
( f is_continuous_in x iff ft is_continuous_at xt )
proofend;

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 )
proofend;

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 &amp; 0. it = 0. X &amp; the addF of it = the addF of X &amp; the Mult of it = the Mult of X &amp; the topology of it = the topology of (TopSpaceNorm X) );
existence
 ex b1 being non empty strict RLTopStruct st
( the carrier of b1 = the carrier of X &amp; 0. b1 = 0. X &amp; the addF of b1 = the addF of X &amp; the Mult of b1 = the Mult of X &amp; the topology of b1 = the topology of (TopSpaceNorm X) )
proofend;
uniqueness
 for b1, b2 being non empty strict RLTopStruct st the carrier of b1 = the carrier of X &amp; 0. b1 = 0. X &amp; the addF of b1 = the addF of X &amp; the Mult of b1 = the Mult of X &amp; the topology of b1 = the topology of (TopSpaceNorm X) &amp; the carrier of b2 = the carrier of X &amp; 0. b2 = 0. X &amp; the addF of b2 = the addF of X &amp; the Mult of b2 = the Mult of X &amp; the topology of b2 = the topology of (TopSpaceNorm X) holds
b1 = b2 ;
end;

:: deftheorem Def4 defines LinearTopSpaceNorm NORMSP_2:def_4_:_
 for X being RealNormSpace
for b2 being non empty strict RLTopStruct holds
( b2 = LinearTopSpaceNorm X iff ( the carrier of b2 = the carrier of X &amp; 0. b2 = 0. X &amp; the addF of b2 = the addF of X &amp; the Mult of b2 = the Mult of X &amp; the topology of b2 = 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 &amp; LinearTopSpaceNorm X is Mult-continuous &amp; LinearTopSpaceNorm X is TopSpace-like &amp; LinearTopSpaceNorm X is Abelian &amp; LinearTopSpaceNorm X is add-associative &amp; LinearTopSpaceNorm X is right_zeroed &amp; LinearTopSpaceNorm X is right_complementable &amp; LinearTopSpaceNorm X is vector-distributive &amp; LinearTopSpaceNorm X is scalar-distributive &amp; LinearTopSpaceNorm X is scalar-associative &amp; LinearTopSpaceNorm X is scalar-unital );
proofend;
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 )
proofend;

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 )
proofend;

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 &amp;  {  y where y is Point of X : ||.(x - y).|| < r  }  c= V ) )
proofend;

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
proofend;

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
proofend;

registration
let X be RealNormSpace;
cluster LinearTopSpaceNorm X ->  non empty T_2 strict ;
coherence
 LinearTopSpaceNorm X is T_2
proofend;
cluster LinearTopSpaceNorm X ->  non empty sober strict ;
coherence
 LinearTopSpaceNorm X is sober by YELLOW_8:22;
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 &amp; x = xt holds
( St is Basis of iff S is Basis of )
proofend;

registration
let X be RealNormSpace;
cluster LinearTopSpaceNorm X ->  non empty first-countable strict ;
coherence
 LinearTopSpaceNorm X is first-countable
proofend;
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 &amp; x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )
proofend;

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 )
proofend;

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 &amp; St is convergent holds
( Lim S = Lim St &amp; lim S = lim St )
proofend;

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 &amp; 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 )
proofend;

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 )
proofend;

theorem :: NORMSP_2:31
for X being RealNormSpace
for S being sequence of X
for St being sequence of (LinearTopSpaceNorm X) st S = St &amp; St is convergent holds
( Lim St = {(lim S)} &amp; lim St = lim S )
proofend;

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 )
proofend;

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 )
proofend;

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 &amp; x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )
proofend;

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 &amp; x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )
proofend;

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 )
proofend;