:: Real Linear Space of Real Sequences
:: by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama
::
:: Received April 3, 2003
:: Copyright (c) 2003 Association of Mizar Users
:: deftheorem Def1 defines the_set_of_RealSequences RSSPACE:def 1 :
:: deftheorem Def2 defines seq_id RSSPACE:def 2 :
:: deftheorem Def3 defines R_id RSSPACE:def 3 :
theorem Th1: :: RSSPACE:1
theorem Th2: :: RSSPACE:2
:: deftheorem Def4 defines l_add RSSPACE:def 4 :
definition
func l_mult -> Function of
[:REAL ,the_set_of_RealSequences :],
the_set_of_RealSequences means :
Def5:
:: RSSPACE:def 5
for
r,
x being
set st
r in REAL &
x in the_set_of_RealSequences holds
it . r,
x = (R_id r) (#) (seq_id x);
existence
ex b1 being Function of [:REAL ,the_set_of_RealSequences :], the_set_of_RealSequences st
for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b1 . r,x = (R_id r) (#) (seq_id x)
by Th2;
uniqueness
for b1, b2 being Function of [:REAL ,the_set_of_RealSequences :], the_set_of_RealSequences st ( for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b1 . r,x = (R_id r) (#) (seq_id x) ) & ( for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b2 . r,x = (R_id r) (#) (seq_id x) ) holds
b1 = b2
end;
:: deftheorem Def5 defines l_mult RSSPACE:def 5 :
:: deftheorem Def6 defines Zeroseq RSSPACE:def 6 :
theorem Th3: :: RSSPACE:3
theorem :: RSSPACE:4
theorem Th5: :: RSSPACE:5
theorem Th6: :: RSSPACE:6
theorem Th7: :: RSSPACE:7
theorem Th8: :: RSSPACE:8
theorem Th9: :: RSSPACE:9
theorem Th10: :: RSSPACE:10
theorem Th11: :: RSSPACE:11
theorem Th12: :: RSSPACE:12
:: deftheorem defines Linear_Space_of_RealSequences RSSPACE:def 7 :
:: deftheorem Def8 defines Add_ RSSPACE:def 8 :
:: deftheorem Def9 defines Mult_ RSSPACE:def 9 :
:: deftheorem Def10 defines Zero_ RSSPACE:def 10 :
theorem Th13: :: RSSPACE:13
:: deftheorem Def11 defines the_set_of_l2RealSequences RSSPACE:def 11 :
theorem :: RSSPACE:14
canceled;
theorem :: RSSPACE:15
theorem Th16: :: RSSPACE:16
theorem :: RSSPACE:17
theorem Th18: :: RSSPACE:18
definition
func l_scalar -> Function of
[:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :],
REAL means :: RSSPACE:def 12
for
x,
y being
set st
x in the_set_of_l2RealSequences &
y in the_set_of_l2RealSequences holds
it . x,
y = Sum ((seq_id x) (#) (seq_id y));
existence
ex b1 being Function of [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :], REAL st
for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . x,y = Sum ((seq_id x) (#) (seq_id y))
by Th18;
uniqueness
for b1, b2 being Function of [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :], REAL st ( for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . x,y = Sum ((seq_id x) (#) (seq_id y)) ) & ( for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b2 . x,y = Sum ((seq_id x) (#) (seq_id y)) ) holds
b1 = b2
end;
:: deftheorem defines l_scalar RSSPACE:def 12 :
registration
cluster UNITSTR(#
the_set_of_l2RealSequences ,
(Zero_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),
(Add_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),
(Mult_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),
l_scalar #)
-> non
empty ;
coherence
not UNITSTR(# the_set_of_l2RealSequences ,(Zero_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),l_scalar #) is empty
;
end;
definition
func l2_Space -> non
empty UNITSTR equals :: RSSPACE:def 13
UNITSTR(#
the_set_of_l2RealSequences ,
(Zero_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),
(Add_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),
(Mult_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),
l_scalar #);
coherence
UNITSTR(# the_set_of_l2RealSequences ,(Zero_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l2RealSequences ,Linear_Space_of_RealSequences ),l_scalar #) is non empty UNITSTR
;
end;
:: deftheorem defines l2_Space RSSPACE:def 13 :
theorem Th19: :: RSSPACE:19
theorem :: RSSPACE:20
theorem :: RSSPACE:21