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


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 Nat holds (Y . n) ` in Family_open_set X ) holds
ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
proof end;

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).||
proof end;
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
proof end;
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
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 by Lm1, Lm2, Lm3, Lm4, METRIC_1:def 6, METRIC_1:def 7, METRIC_1:def 8, METRIC_1:def 9;
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 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 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 Nat st
for n being 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;

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;

:: 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
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 Nat st
for n being 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;

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 b1 being non empty strict RLTopStruct st
( the carrier of b1 = the carrier of X & 0. b1 = 0. X & the addF of b1 = the addF of X & the Mult of b1 = the Mult of X & the topology of b1 = the topology of (TopSpaceNorm X) )
proof end;
uniqueness
for b1, b2 being non empty strict RLTopStruct st the carrier of b1 = the carrier of X & 0. b1 = 0. X & the addF of b1 = the addF of X & the Mult of b1 = the Mult of X & the topology of b1 = the topology of (TopSpaceNorm X) & the carrier of b2 = the carrier of X & 0. b2 = 0. X & the addF of b2 = the addF of X & the Mult of b2 = the Mult of X & 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 & 0. b2 = 0. X & the addF of b2 = the addF of X & the Mult of b2 = the Mult of X & 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 & 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 ) by Def4;

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: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 & 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 Nat st
for n being 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;