begin
:: deftheorem Def1 defines the_set_of_l1RealSequences RSSPACE3:def 1 :
theorem Th1:
Lm1:
RLSStruct(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ) #) is Subspace of Linear_Space_of_RealSequences
by RSSPACE:13;
registration
cluster RLSStruct(#
the_set_of_l1RealSequences ,
(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),
(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),
(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ) #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ) #) is Abelian & RLSStruct(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ) #) is add-associative & RLSStruct(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ) #) is right_zeroed & RLSStruct(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ) #) is right_complementable & RLSStruct(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ) #) is vector-distributive & RLSStruct(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ) #) is scalar-distributive & RLSStruct(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ) #) is scalar-associative & RLSStruct(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ) #) is scalar-unital )
by RSSPACE:13;
end;
Lm2:
RLSStruct(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ) #) is RealLinearSpace
;
Lm3:
ex NORM being Function of the_set_of_l1RealSequences ,REAL st
for x being set st x in the_set_of_l1RealSequences holds
NORM . x = Sum (abs (seq_id x))
:: deftheorem Def2 defines l_norm RSSPACE3:def 2 :
registration
let X be non
empty set ;
let Z be
Element of
X;
let A be
BinOp of
X;
let M be
Function of
[:REAL ,X:],
X;
let N be
Function of
X,
REAL ;
cluster NORMSTR(#
X,
Z,
A,
M,
N #)
-> non
empty ;
coherence
not NORMSTR(# X,Z,A,M,N #) is empty
;
end;
theorem
canceled;
theorem
canceled;
theorem
theorem Th5:
theorem Th6:
theorem Th7:
definition
func l1_Space -> non
empty NORMSTR equals
NORMSTR(#
the_set_of_l1RealSequences ,
(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),
(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),
(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),
l_norm #);
coherence
NORMSTR(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),l_norm #) is non empty NORMSTR
;
end;
:: deftheorem defines l1_Space RSSPACE3:def 3 :
begin
theorem Th8:
theorem Th9:
Lm4:
for c being Real
for seq, seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) )
:: deftheorem defines dist RSSPACE3:def 4 :
:: deftheorem Def5 defines CCauchy RSSPACE3:def 5 :
theorem Th10:
theorem