The abstract of the Mizar article:

Real Linear Space of Real Sequences

by

Noboru Endou,

Yasumasa Suzuki, and

Yasunari Shidama

Received April 3, 2003

MML identifier: RSSPACE

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, FUNCT_1, ARYTM, ARYTM_1, RELAT_1, ABSVALUE, ORDINAL2,
      BINOP_1, SQUARE_1, PROB_1, FUNCT_2, RLSUB_1, SEQ_1, SEQ_2, SERIES_1,
      BHSP_1, SUPINF_2, RSSPACE;
 notation TARSKI, SUBSET_1, XBOOLE_0, ZFMISC_1, ORDINAL1, NUMBERS, XREAL_0,
      STRUCT_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, RLVECT_1,
      ABSVALUE, RLSUB_1, BHSP_1, SQUARE_1, SEQ_1, SEQ_2, SEQM_3, SERIES_1,
      BINOP_1;
 constructors REAL_1, NAT_1, DOMAIN_1, SQUARE_1, SEQ_2, SERIES_1, PREPOWER,
      PARTFUN1, BINOP_1, RLSUB_1, BHSP_3, MEMBERED;
 clusters RELSET_1, STRUCT_0, RLVECT_1, SEQ_1, BHSP_1, XREAL_0, MEMBERED;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin

definition
 func the_set_of_RealSequences -> non empty set means
:: RSSPACE:def 1
  for x being set holds x in it iff x is Real_Sequence;
end;

definition
  let a be set such that
  a in the_set_of_RealSequences;
  func seq_id(a) -> Real_Sequence equals
:: RSSPACE:def 2
   a;
end;

definition
 let a be set such that
 a in REAL;
 func R_id(a) -> Real equals
:: RSSPACE:def 3
  a;
end;

theorem :: RSSPACE:1
ex ADD be BinOp of the_set_of_RealSequences st
  (for a,b being Element of the_set_of_RealSequences
    holds ADD.(a,b) = seq_id(a)+seq_id(b)) & ADD is commutative associative;

theorem :: RSSPACE:2
ex f be Function of [: REAL, the_set_of_RealSequences :],
  the_set_of_RealSequences st
   for r,x be set st r in REAL & x in the_set_of_RealSequences
      holds f.[r,x] = R_id(r) (#) seq_id(x);

definition
  func l_add -> BinOp of the_set_of_RealSequences means
:: RSSPACE:def 4
    for a,b being Element of the_set_of_RealSequences holds
      it.(a,b) = seq_id(a)+seq_id(b);
end;

definition
 func l_mult -> Function of [: REAL, the_set_of_RealSequences :],
  the_set_of_RealSequences means
:: RSSPACE:def 5
   for r,x be set st r in REAL & x in the_set_of_RealSequences
      holds it.[r,x] = R_id(r)(#)seq_id(x);
end;

definition
 func Zeroseq -> Element of the_set_of_RealSequences means
:: RSSPACE:def 6
 for n be Nat holds (seq_id it).n=0;
end;

theorem :: RSSPACE:3
for x be Real_Sequence holds seq_id x = x;

theorem :: RSSPACE:4
for v,w being VECTOR of
 RLSStruct(#the_set_of_RealSequences,Zeroseq,l_add,l_mult#) holds
  v + w = seq_id(v)+seq_id(w);

theorem :: RSSPACE:5
for r being Real,
 v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)
  holds r * v = r(#)seq_id(v);

definition
  cluster RLSStruct (# the_set_of_RealSequences, Zeroseq, l_add, l_mult #) ->
    Abelian;
end;

theorem :: RSSPACE:6
for u,v,w being VECTOR of
 RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds
  (u + v) + w = u + (v + w);

theorem :: RSSPACE:7
for v being VECTOR of
 RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds
  v + 0.RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) = v;

theorem :: RSSPACE:8
for v being VECTOR of
 RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)
  ex w being VECTOR of
   RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) st
    v + w = 0.RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);

theorem :: RSSPACE:9
for a being Real, v,w being VECTOR of
 RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds
  a * (v + w) = a * v + a * w;

theorem :: RSSPACE:10
for a,b being Real, v being VECTOR of
 RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds
  (a + b) * v = a * v + b * v;

theorem :: RSSPACE:11
for a,b be Real, v being VECTOR of
 RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds
  (a * b) * v = a * (b * v);

theorem :: RSSPACE:12
for v being VECTOR of
 RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds 1 * v = v;

definition
  func Linear_Space_of_RealSequences -> RealLinearSpace equals
:: RSSPACE:def 7
   RLSStruct (# the_set_of_RealSequences, Zeroseq, l_add, l_mult #);
end;

definition
let X be RealLinearSpace;
let X1 be Subset of X such that
X1 is lineary-closed & X1 is non empty;
func Add_(X1,X) -> BinOp of X1 equals
:: RSSPACE:def 8
(the add of X) | [:X1,X1:];
end;

definition
let X be RealLinearSpace;
let X1 be Subset of X such that
 X1 is lineary-closed & X1 is non empty;
func Mult_(X1,X) -> Function of [:REAL,X1:], X1 equals
:: RSSPACE:def 9
(the Mult of X) | [:REAL,X1:];
end;

definition
let X be RealLinearSpace, X1 be Subset of X such that
 X1 is lineary-closed & X1 is non empty;
func Zero_(X1,X) -> Element of X1 equals
:: RSSPACE:def 10
  0.X;
end;

theorem :: RSSPACE:13
for V be RealLinearSpace, V1 be Subset of V
 st V1 is lineary-closed & V1 is non empty holds
  RLSStruct (# V1,Zero_(V1,V), Add_(V1,V),Mult_(V1,V) #) is Subspace of V;

definition
  func the_set_of_l2RealSequences -> Subset of
  Linear_Space_of_RealSequences means
:: RSSPACE:def 11
  it is non empty &
  for x being set holds x in it iff
  (x in the_set_of_RealSequences &
  seq_id(x)(#)seq_id(x) is summable);
end;

theorem :: RSSPACE:14
the_set_of_l2RealSequences is lineary-closed &
 the_set_of_l2RealSequences is non empty;

theorem :: RSSPACE:15
  RLSStruct(# 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) #)
is Subspace of Linear_Space_of_RealSequences;

theorem :: RSSPACE:16
RLSStruct (# 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) #)
is RealLinearSpace;

theorem :: RSSPACE:17
   the carrier of Linear_Space_of_RealSequences = the_set_of_RealSequences &
(for x be set holds
  x is Element of Linear_Space_of_RealSequences
  iff x is Real_Sequence )
& (for x be set holds x is VECTOR of Linear_Space_of_RealSequences
  iff x is Real_Sequence )
&(for u be VECTOR of Linear_Space_of_RealSequences
  holds u =seq_id(u) )
&(for u,v be VECTOR of Linear_Space_of_RealSequences
  holds u+v =seq_id(u)+seq_id(v) )
&( for r be Real for u be VECTOR of Linear_Space_of_RealSequences
  holds r*u =r(#)seq_id(u) );

theorem :: RSSPACE:18
ex f be Function of
[: the_set_of_l2RealSequences, the_set_of_l2RealSequences :], REAL st
  ( for x,y be set st
        x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences
      holds f.[x,y] = Sum(seq_id(x)(#)seq_id(y)) );

definition
 func l_scalar -> Function of
  [:the_set_of_l2RealSequences, the_set_of_l2RealSequences:], REAL means
:: RSSPACE:def 12
    (for x,y be 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)));
end;

definition
  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;
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 #);
end;

theorem :: RSSPACE:19
for l be UNITSTR st
RLSStruct (# the carrier of l, the Zero of l, the add of l,
        the Mult of l #) is RealLinearSpace holds l is RealLinearSpace;

theorem :: RSSPACE:20
  for rseq be Real_Sequence
   st (for n be Nat holds rseq.n=0) holds
   rseq is summable & Sum rseq = 0;

theorem :: RSSPACE:21
  for rseq be Real_Sequence
   st ( (for n be Nat holds 0 <= rseq.n) & rseq is summable & Sum rseq=0)
   holds for n be Nat holds rseq.n =0;

definition
  cluster l2_Space -> Abelian add-associative right_zeroed
    right_complementable RealLinearSpace-like;
end;