:: Separability of Real Normed Spaces and Its Basic Properties
:: by Kazuhisa Nakasho and Noboru Endou
::
:: Received February 26, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

definition

let X be RealLinearSpace;
let A be Subset of X;

func RAT_Sums A -> Subset of X equals :: NORMSP_4:def 1
{ (Sum l) where l is Linear_Combination of A : rng l c= RAT } ;

correctness
coherence
{ (Sum l) where l is Linear_Combination of A : rng l c= RAT } is Subset of X;

proof end;

end;

:: deftheorem defines RAT_Sums NORMSP_4:def 1 :
for X being RealLinearSpace
for A being Subset of X holds RAT_Sums A = { (Sum l) where l is Linear_Combination of A : rng l c= RAT } ;

theorem Th1: :: NORMSP_4:1

for V being RealNormSpace
for V1 being SubRealNormSpace of V holds TopSpaceNorm V1 is SubSpace of TopSpaceNorm V

proof end;

theorem Th2: :: NORMSP_4:2

for V being RealNormSpace
for V1 being SubRealNormSpace of V holds LinearTopSpaceNorm V1 is SubSpace of LinearTopSpaceNorm V

proof end;

theorem Th3: :: NORMSP_4:3

for X being RealNormSpace
for Y, Z being SubRealNormSpace of X st ex A being Subset of X st
( A = the carrier of Y & Cl A = the carrier of Z ) holds
for D0 being Subset of Y
for D being Subset of Z st D0 is dense & D0 = D holds
D is dense

proof end;

theorem Th4: :: NORMSP_4:4

for X being addLoopStr
for A, B being Subset of X ex F being Function of (A + B),[:A,B:] st F is one-to-one

proof end;

theorem Th5: :: NORMSP_4:5

for X being addLoopStr
for A, B being Subset of X st A is countable & B is countable holds
A + B is countable

proof end;

Lm6: for X being RealLinearSpace
for v being Element of the carrier of X holds RAT_Sums {v} is countable

proof end;

theorem Th7: :: NORMSP_4:6

for X being non empty addLoopStr
for A, B being Subset of X
for l1 being Linear_Combination of A
for l2 being Linear_Combination of B st A misses B holds
ex l being Linear_Combination of A \/ B st
( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 )

proof end;

theorem Th8: :: NORMSP_4:7

for X being non empty addLoopStr
for A, B being Subset of X
for l being Linear_Combination of A \/ B ex l1 being Linear_Combination of A st
( Carrier l1 = (Carrier l) \ B & ( for x being Element of X st x in Carrier l1 holds
l1 . x = l . x ) )

proof end;

theorem Th9: :: NORMSP_4:8

for X being non empty addLoopStr
for A, B being Subset of X
for l being Linear_Combination of A \/ B st A misses B holds
ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st
( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )

proof end;

theorem Th10: :: NORMSP_4:9

for X being RealLinearSpace
for A, B being Subset of X
for l1 being Linear_Combination of A
for l2 being Linear_Combination of B st rng l1 c= RAT & rng l2 c= RAT & A misses B holds
ex l being Linear_Combination of A \/ B st
( Carrier l = (Carrier l1) \/ (Carrier l2) & rng l c= RAT & Sum l = (Sum l1) + (Sum l2) )

proof end;

theorem Th11: :: NORMSP_4:10

for X being RealLinearSpace
for A, B being Subset of X
for l being Linear_Combination of A \/ B st rng l c= RAT & A misses B holds
ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st
( rng l1 c= RAT & rng l2 c= RAT & Sum l = (Sum l1) + (Sum l2) )

proof end;

theorem Th12: :: NORMSP_4:11

for X being RealLinearSpace
for A, B being finite Subset of X st A misses B holds
(RAT_Sums A) + (RAT_Sums B) = RAT_Sums (A \/ B)

proof end;

Lm13: for X being RealLinearSpace holds RAT_Sums ({} X) is countable

proof end;

Th14: for X being RealLinearSpace
for A being finite Subset of X holds RAT_Sums A is countable

proof end;

registration

let X be RealLinearSpace;
let A be finite Subset of X;

cluster RAT_Sums A -> countable ;

coherence
RAT_Sums A is countable by Th14;

end;

theorem Th15: :: NORMSP_4:12

for X being RealLinearSpace
for x being sequence of X
for A being finite Subset of X st A c= rng x holds
ex n being Nat st A c= rng (x | (Segm n))

proof end;

Th16: for X being RealLinearSpace
for x being sequence of X holds RAT_Sums (rng x) is countable

proof end;

registration

let X be RealLinearSpace;
let x be sequence of X;

cluster RAT_Sums (rng x) -> countable ;

coherence
RAT_Sums (rng x) is countable by Th16;

end;

theorem Th17: :: NORMSP_4:13

for X being RealNormSpace
for x being sequence of X holds RAT_Sums (rng x) is Subset of the carrier of (NLin (rng x))

proof end;

theorem Th18: :: NORMSP_4:14

for X being RealNormSpace
for Y being Subset of X holds
( the carrier of (NLin Y) c= the carrier of (ClNLin Y) & ex Z being Subset of X st
( Z = the carrier of (NLin Y) & Cl Z = the carrier of (ClNLin Y) ) )

proof end;

theorem Th19: :: NORMSP_4:15

for X being RealNormSpace
for x being sequence of X holds RAT_Sums (rng x) is countable Subset of the carrier of (ClNLin (rng x))

proof end;

theorem Th21: :: NORMSP_4:16

for z, e being Real st 0 < e holds
ex q being Element of RAT st
( q <> 0 & |.(z - q).| < e )

proof end;

theorem Th22: :: NORMSP_4:17

for X being RealNormSpace
for w being Point of X
for e being Real
for l being Linear_Combination of {w} st 0 < e holds
ex m being Linear_Combination of {w} st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

proof end;

theorem Th23: :: NORMSP_4:18

for X being RealNormSpace
for A being Subset of X
for e being Real
for l being Linear_Combination of A st 0 < e holds
ex m being Linear_Combination of A st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

proof end;

Th24: for X being RealNormSpace
for x being sequence of X
for D being Subset of the carrier of (NLin (rng x)) st D = RAT_Sums (rng x) holds
D is dense

proof end;

theorem :: NORMSP_4:19

for X being RealNormSpace
for x being sequence of X holds RAT_Sums (rng x) is dense Subset of the carrier of (NLin (rng x)) by Th17, Th24;

Th25: for X being RealNormSpace
for x being sequence of X
for D being Subset of the carrier of (ClNLin (rng x)) st D = RAT_Sums (rng x) holds
D is dense

proof end;

theorem :: NORMSP_4:20

for X being RealNormSpace
for x being sequence of X holds RAT_Sums (rng x) is dense Subset of the carrier of (ClNLin (rng x)) by Th19, Th25;

theorem Th26: :: NORMSP_4:21

for X being RealNormSpace st ex D being Subset of the carrier of X st
( D is dense & D is countable ) holds
X is separable

proof end;

registration

let X be RealNormSpace;
let x be sequence of X;

cluster ClNLin (rng x) -> separable ;

coherence
ClNLin (rng x) is separable

proof end;

end;

theorem :: NORMSP_4:22

for X being RealNormSpace
for Y being SubRealNormSpace of X
for L being Lipschitzian linear-Functional of X holds L | the carrier of Y is Lipschitzian linear-Functional of Y

proof end;

Th29: for X, Y being RealNormSpace
for A being Subset of X
for B being Subset of Y
for L being Lipschitzian LinearOperator of X,Y st L is isomorphism & B = L .: A & A is dense holds
B is dense

proof end;

theorem Th30: :: NORMSP_4:23

for X, Y being RealNormSpace
for A being Subset of X
for B being Subset of Y
for L being Lipschitzian LinearOperator of X,Y st L is isomorphism & B = L .: A holds
( A is dense iff B is dense )

proof end;

theorem Th31: :: NORMSP_4:24

for X, Y being RealNormSpace st ex L being Lipschitzian LinearOperator of X,Y st L is isomorphism holds
( X is separable iff Y is separable )

proof end;

theorem :: NORMSP_4:25

for X being RealNormSpace st not X is trivial & X is Reflexive holds
( X is separable iff DualSp (DualSp X) is separable )

proof end;

theorem :: NORMSP_4:26

for X being RealNormSpace
for Y, Z being Subset of X st Z = the carrier of (Lin Y) holds
the carrier of (Lin Z) = Z by RLVECT_3:18;

theorem Th35: :: NORMSP_4:27

for X being RealBanachSpace
for Y being Subset of X ex Z being Subset of X st
( Z = the carrier of (Lin Y) & ClNLin Y = NLin (Cl Z) & Cl Z is linearly-closed & Cl Z <> {} )

proof end;

theorem :: NORMSP_4:28

for X being RealBanachSpace
for Y being Subset of X holds ClNLin Y is RealBanachSpace

proof end;

theorem :: NORMSP_4:29

for X being RealBanachSpace
for Y being Subset of X st X is Reflexive holds
ClNLin Y is Reflexive

proof end;