begin
theorem
theorem Th2:
theorem Th3:
:: deftheorem Def1 defines MultOps PRVECT_2:def 1 :
theorem Th4:
theorem Th5:
definition
let F be
Domain-Sequence;
let X be non
empty set ;
let p be
MultOps of
X,
F;
func [:p:] -> Function of
[:X,(product F):],
product F means :
Def2:
for
x being
Element of
X for
d being
Element of
product F for
i being
Element of
dom F holds
(it . x,d) . i = (p . i) . x,
(d . i);
existence
ex b1 being Function of [:X,(product F):], product F st
for x being Element of X
for d being Element of product F
for i being Element of dom F holds (b1 . x,d) . i = (p . i) . x,(d . i)
uniqueness
for b1, b2 being Function of [:X,(product F):], product F st ( for x being Element of X
for d being Element of product F
for i being Element of dom F holds (b1 . x,d) . i = (p . i) . x,(d . i) ) & ( for x being Element of X
for d being Element of product F
for i being Element of dom F holds (b2 . x,d) . i = (p . i) . x,(d . i) ) holds
b1 = b2
end;
:: deftheorem Def2 defines [: PRVECT_2:def 2 :
:: deftheorem Def3 defines RealLinearSpace-yielding PRVECT_2:def 3 :
:: deftheorem Def4 defines carr PRVECT_2:def 4 :
:: deftheorem Def5 defines addop PRVECT_2:def 5 :
:: deftheorem Def6 defines complop PRVECT_2:def 6 :
:: deftheorem Def7 defines zeros PRVECT_2:def 7 :
:: deftheorem Def8 defines multop PRVECT_2:def 8 :
:: deftheorem defines product PRVECT_2:def 9 :
Lm1:
for LS being non empty addLoopStr st the addF of LS is commutative & the addF of LS is associative holds
( LS is Abelian & LS is add-associative )
Lm2:
for LS being non empty addLoopStr st the ZeroF of LS is_a_unity_wrt the addF of LS holds
LS is right_zeroed
Lm3:
for G being RealLinearSpace-Sequence
for v1, w1 being Element of product (carr G)
for i being Element of dom (carr G) holds
( ([:(addop G):] . v1,w1) . i = the addF of (G . i) . (v1 . i),(w1 . i) & ( for vi, wi being VECTOR of st vi = v1 . i & wi = w1 . i holds
([:(addop G):] . v1,w1) . i = vi + wi ) )
Lm4:
for G being RealLinearSpace-Sequence
for r being Real
for v being Element of product (carr G)
for i being Element of dom (carr G) holds
( ([:(multop G):] . r,v) . i = the Mult of (G . i) . r,(v . i) & ( for vi being VECTOR of st vi = v . i holds
([:(multop G):] . r,v) . i = r * vi ) )
Lm5:
for G being RealLinearSpace-Sequence holds product G is RealLinearSpace-like
begin
:: deftheorem Def10 defines RealNormSpace-yielding PRVECT_2:def 10 :
Lm6:
for g being RealNormSpace-yielding FinSequence holds g is RealLinearSpace-yielding
:: deftheorem Def11 defines normsequence PRVECT_2:def 11 :
:: deftheorem Def12 defines productnorm PRVECT_2:def 12 :
definition
let G be
RealNormSpace-Sequence;
func product G -> non
empty strict NORMSTR means :
Def13:
(
RLSStruct(# the
carrier of
it,the
ZeroF of
it,the
addF of
it,the
Mult of
it #)
= product G & the
norm of
it = productnorm G );
existence
ex b1 being non empty strict NORMSTR st
( RLSStruct(# the carrier of b1,the ZeroF of b1,the addF of b1,the Mult of b1 #) = product G & the norm of b1 = productnorm G )
uniqueness
for b1, b2 being non empty strict NORMSTR st RLSStruct(# the carrier of b1,the ZeroF of b1,the addF of b1,the Mult of b1 #) = product G & the norm of b1 = productnorm G & RLSStruct(# the carrier of b2,the ZeroF of b2,the addF of b2,the Mult of b2 #) = product G & the norm of b2 = productnorm G holds
b1 = b2
;
end;
:: deftheorem Def13 defines product PRVECT_2:def 13 :
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
Lm7:
for G being RealNormSpace-Sequence holds product G is RealNormSpace-like
theorem Th10:
Lm8:
for RNS being RealNormSpace
for S being sequence of RNS
for g being Point of holds
( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) )
theorem Th11:
theorem
theorem Th13:
theorem