:: Separability of Real Normed Spaces and Its Basic Properties
:: by Kazuhisa Nakasho and Noboru Endou
::
:: Copyright (c) 2015-2019 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 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 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 = () \ 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 = () \ B & Carrier l2 = () \ 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 \/ 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;
coherence 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 () & ex Z being Subset of X st
( Z = the carrier of (NLin Y) & Cl Z = the carrier of () ) )
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 ;

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 ;

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