:: 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 )

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;

ex b_{1} being Function of [: the carrier of X, the carrier of X:],REAL st

for x, y being Point of X holds b_{1} . (x,y) = ||.(x - y).||

for b_{1}, b_{2} being Function of [: the carrier of X, the carrier of X:],REAL st ( for x, y being Point of X holds b_{1} . (x,y) = ||.(x - y).|| ) & ( for x, y being Point of X holds b_{2} . (x,y) = ||.(x - y).|| ) holds

b_{1} = b_{2}

end;
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 for x, y being Point of X holds it . (x,y) = ||.(x - y).||;

ex b

for x, y being Point of X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines distance_by_norm_of NORMSP_2:def 1 :

for X being RealNormSpace

for b_{2} being Function of [: the carrier of X, the carrier of X:],REAL holds

( b_{2} = distance_by_norm_of X iff for x, y being Point of X holds b_{2} . (x,y) = ||.(x - y).|| );

for X being RealNormSpace

for b

( b

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;

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

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;

:: deftheorem defines MetricSpaceNorm NORMSP_2:def 2 :

for X being RealNormSpace holds MetricSpaceNorm X = MetrStruct(# the carrier of X,(distance_by_norm_of X) #);

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 } )

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 } )

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 )

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 )

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

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;

TopSpaceMetr (MetricSpaceNorm X) is non empty TopSpace ;

end;
func TopSpaceNorm X -> non empty TopSpace equals :: NORMSP_2:def 3

TopSpaceMetr (MetricSpaceNorm X);

coherence TopSpaceMetr (MetricSpaceNorm X);

TopSpaceMetr (MetricSpaceNorm X) is non empty TopSpace ;

:: deftheorem defines TopSpaceNorm NORMSP_2:def 3 :

for X being RealNormSpace holds TopSpaceNorm X = TopSpaceMetr (MetricSpaceNorm X);

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

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)

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)

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;

:: Baire Category Theorem (Hausdorff spaces)

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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;

ex b_{1} being non empty strict RLTopStruct st

( the carrier of b_{1} = the carrier of X & 0. b_{1} = 0. X & the addF of b_{1} = the addF of X & the Mult of b_{1} = the Mult of X & the topology of b_{1} = the topology of (TopSpaceNorm X) )

for b_{1}, b_{2} being non empty strict RLTopStruct st the carrier of b_{1} = the carrier of X & 0. b_{1} = 0. X & the addF of b_{1} = the addF of X & the Mult of b_{1} = the Mult of X & the topology of b_{1} = the topology of (TopSpaceNorm X) & the carrier of b_{2} = the carrier of X & 0. b_{2} = 0. X & the addF of b_{2} = the addF of X & the Mult of b_{2} = the Mult of X & the topology of b_{2} = the topology of (TopSpaceNorm X) holds

b_{1} = b_{2}
;

end;
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 ( 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) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def4 defines LinearTopSpaceNorm NORMSP_2:def 4 :

for X being RealNormSpace

for b_{2} being non empty strict RLTopStruct holds

( b_{2} = LinearTopSpaceNorm X iff ( the carrier of b_{2} = the carrier of X & 0. b_{2} = 0. X & the addF of b_{2} = the addF of X & the Mult of b_{2} = the Mult of X & the topology of b_{2} = the topology of (TopSpaceNorm X) ) );

for X being RealNormSpace

for b

( b

registration

let X be RealNormSpace;

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

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

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;

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 )

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

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

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

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;

coherence

LinearTopSpaceNorm X is T_2

LinearTopSpaceNorm X is sober by YELLOW_8:22;

end;
coherence

LinearTopSpaceNorm X is T_2

proof end;

coherence LinearTopSpaceNorm X is sober by YELLOW_8:22;

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 )

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;

coherence

LinearTopSpaceNorm X is first-countable

LinearTopSpaceNorm X is Frechet ;

coherence

LinearTopSpaceNorm X is sequential ;

end;
coherence

LinearTopSpaceNorm X is first-countable

proof end;

coherence LinearTopSpaceNorm X is Frechet ;

coherence

LinearTopSpaceNorm X is sequential ;

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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;