:: by Kazuhisa Nakasho and Noboru Endou

::

:: Received February 26, 2015

:: Copyright (c) 2015-2016 Association of Mizar Users

definition

let X be RealLinearSpace;

let A be Subset of X;

coherence

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

end;
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 { (Sum l) where l is Linear_Combination of A : rng l c= RAT } ;

coherence

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

proof 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 } ;

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

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

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

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

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

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 )

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

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 )

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

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

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)

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

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

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

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

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

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 )

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 )

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

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

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

( D is dense & D is countable ) holds

X is separable

proof end;

registration
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

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 )

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 )

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

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

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

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;