:: 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-2018 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, #) is Reflexive
proof end;

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

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

Lm4: for X being RealNormSpace holds the distance of MetrStruct(# the carrier 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, #);
coherence
MetrStruct(# the carrier of X, #) is non empty MetrSpace
by ;
end;

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

theorem Th2: :: NORMSP_2:2
for X being RealNormSpace
for z being Element of ()
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 ()
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 ()
for x being Point of X
for xt being Point of () 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 () 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 () st S = St & St is convergent holds
lim St = lim S
proof end;

definition
let X be RealNormSpace;
coherence
TopSpaceMetr () is non empty TopSpace
;
end;

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

theorem Th7: :: NORMSP_2:7
for X being RealNormSpace
for V being Subset of () 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 ()
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 ()
proof end;

:: 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;
coherence ;
end;

theorem Th12: :: NORMSP_2:12
for X being RealNormSpace
for S being sequence of X
for St being sequence of ()
for x being Point of X
for xt being Point of () 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 () 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 () 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 () 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 () 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 ()
for x being Point of X
for xt being Point of () 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 (),()
for x being Point of X
for xt being Point of () 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 (),() 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 () );
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 () )
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 () & 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 () 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 () ) );

registration
let X be RealNormSpace;
correctness
coherence ;
proof end;
end;

theorem Th20: :: NORMSP_2:20
for X being RealNormSpace
for V being Subset of ()
for Vt being Subset of 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 ()
for Vt being Subset of 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 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 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 () st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed
proof end;

registration
let X be RealNormSpace;
coherence
proof end;
coherence by YELLOW_8:22;
end;

theorem Th25: :: NORMSP_2:25
for X being RealNormSpace
for S being Subset-Family of ()
for St being Subset-Family of
for x being Point of ()
for xt being Point of st S = St & x = xt holds
( St is Basis of iff S is Basis of )
proof end;

registration
let X be RealNormSpace;
coherence
proof end;
coherence ;
coherence ;
end;

theorem Th26: :: NORMSP_2:26
for X being RealNormSpace
for S being sequence of ()
for St being sequence of
for x being Point of ()
for xt being Point of 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 ()
for St being sequence of 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 ()
for St being sequence of 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
for x being Point of X
for xt being Point of 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 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 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 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 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 ()
for Ut being Subset of
for x being Point of ()
for xt being Point of 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 (),()
for ft being Function of ,
for x being Point of ()
for xt being Point of 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 (),()
for ft being Function of , st f = ft holds
( f is continuous iff ft is continuous )
proof end;