:: Real Linear Space of Real Sequences
:: by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama
::
:: Copyright (c) 2003-2021 Association of Mizar Users

definition
coherence
Funcs (NAT,REAL) is non empty set
;
end;

:: deftheorem defines the_set_of_RealSequences RSSPACE:def 1 :

definition
let a be object ;
assume A1: a in the_set_of_RealSequences ;
func seq_id a -> Real_Sequence equals :Def2: :: RSSPACE:def 2
a;
coherence by ;
end;

:: deftheorem Def2 defines seq_id RSSPACE:def 2 :
for a being object st a in the_set_of_RealSequences holds
seq_id a = a;

definition
::$CD 3 coherence by FUNCT_2:8; end; :: deftheorem RSSPACE:def 3 : canceled; :: deftheorem RSSPACE:def 4 : canceled; :: deftheorem RSSPACE:def 5 : canceled; :: deftheorem defines Zeroseq RSSPACE:def 6 : registration let x be Element of the_set_of_RealSequences ; reduce seq_id x to x; reducibility seq_id x = x by Def2; end; registration let x be Real_Sequence; reduce seq_id x to x; reducibility seq_id x = x proof end; end; theorem :: RSSPACE:1 for x being Real_Sequence holds seq_id x = x ; definition coherence ; end; :: deftheorem defines Linear_Space_of_RealSequences RSSPACE:def 7 : registration let x be Element of Linear_Space_of_RealSequences; reduce seq_id x to x; reducibility seq_id x = x by Def2; end; registration coherence ; end; theorem :: RSSPACE:2 for v, w being VECTOR of Linear_Space_of_RealSequences holds v + w = () + () proof end; theorem Th3: :: RSSPACE:3 for r being Real for v being VECTOR of Linear_Space_of_RealSequences holds r * v = r (#) () proof end; registration end; definition let X be RealLinearSpace; let X1 be Subset of X; assume A1: ( X1 is linearly-closed & not X1 is empty ) ; func Add_ (X1,X) -> BinOp of X1 equals :Def5: :: RSSPACE:def 8 the addF of X || X1; correctness coherence the addF of X || X1 is BinOp of X1 ; proof end; end; :: deftheorem Def5 defines Add_ RSSPACE:def 8 : for X being RealLinearSpace for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds Add_ (X1,X) = the addF of X || X1; definition let X be RealLinearSpace; let X1 be Subset of X; assume A1: ( X1 is linearly-closed & not X1 is empty ) ; func Mult_ (X1,X) -> Function of [:REAL,X1:],X1 equals :Def6: :: RSSPACE:def 9 the Mult of X | [:REAL,X1:]; correctness coherence the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1 ; proof end; end; :: deftheorem Def6 defines Mult_ RSSPACE:def 9 : for X being RealLinearSpace for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds Mult_ (X1,X) = the Mult of X | [:REAL,X1:]; definition let X be RealLinearSpace; let X1 be Subset of X; assume A1: ( X1 is linearly-closed & not X1 is empty ) ; func Zero_ (X1,X) -> Element of X1 equals :Def7: :: RSSPACE:def 10 0. X; correctness coherence 0. X is Element of X1 ; proof end; end; :: deftheorem Def7 defines Zero_ RSSPACE:def 10 : for X being RealLinearSpace for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds Zero_ (X1,X) = 0. X; theorem :: RSSPACE:4 for n being object holds . n = 0 proof end; theorem :: RSSPACE:5 for f being Element of the_set_of_RealSequences st ( for n being Nat holds () . n = 0 ) holds f = Zeroseq proof end; theorem :: RSSPACE:6 canceled; theorem :: RSSPACE:7 canceled; theorem :: RSSPACE:8 canceled; theorem :: RSSPACE:9 canceled; theorem :: RSSPACE:10 canceled; ::$CT 5
for V being RealLinearSpace
for V1 being Subset of V st V1 is linearly-closed & not V1 is empty holds
RLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V
proof end;

definition
func the_set_of_l2RealSequences -> Subset of Linear_Space_of_RealSequences means :Def8: :: RSSPACE:def 11
for x being object holds
( x in it iff ( x in the_set_of_RealSequences & () (#) () is summable ) );
existence
ex b1 being Subset of Linear_Space_of_RealSequences st
for x being object holds
( x in b1 iff ( x in the_set_of_RealSequences & () (#) () is summable ) )
proof end;
uniqueness
for b1, b2 being Subset of Linear_Space_of_RealSequences st ( for x being object holds
( x in b1 iff ( x in the_set_of_RealSequences & () (#) () is summable ) ) ) & ( for x being object holds
( x in b2 iff ( x in the_set_of_RealSequences & () (#) () is summable ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines the_set_of_l2RealSequences RSSPACE:def 11 :
for b1 being Subset of Linear_Space_of_RealSequences holds
( b1 = the_set_of_l2RealSequences iff for x being object holds
( x in b1 iff ( x in the_set_of_RealSequences & () (#) () is summable ) ) );

registration
coherence
proof end;
end;

canceled;

::\$CT
definition
func l_scalar -> Function of ,REAL means :: RSSPACE:def 12
for x, y being object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
it . (x,y) = Sum (() (#) ());
existence
ex b1 being Function of ,REAL st
for x, y being object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . (x,y) = Sum (() (#) ())
proof end;
uniqueness
for b1, b2 being Function of ,REAL st ( for x, y being object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . (x,y) = Sum (() (#) ()) ) & ( for x, y being object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b2 . (x,y) = Sum (() (#) ()) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines l_scalar RSSPACE:def 12 :
for b1 being Function of ,REAL holds
( b1 = l_scalar iff for x, y being object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . (x,y) = Sum (() (#) ()) );

registration
let x be Element of l2_Space;
reduce seq_id x to x;
reducibility
seq_id x = x
proof end;
end;

for l being RLSStruct st RLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is RealLinearSpace holds
l is RealLinearSpace
proof end;