:: by Kazuhisa Nakasho and Noboru Endou

::

:: Received February 26, 2015

:: Copyright (c) 2015-2018 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

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