begin
theorem
theorem Th2:
theorem Th3:
:: deftheorem Def1 defines MultOps PRVECT_2:def 1 :
for f being Function
for X being set
for b3 being Function holds
( b3 is MultOps of X,f iff ( dom b3 = dom f & ( for i being set st i in dom f holds
b3 . i is Function of [:X,(f . i):],(f . i) ) ) );
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 :
for F being Domain-Sequence
for X being non empty set
for p being MultOps of X,F
for b4 being Function of [:X,(product F):],(product F) holds
( b4 = [:p:] iff for x being Element of X
for d being Element of product F
for i being Element of dom F holds (b4 . x,d) . i = (p . i) . x,(d . i) );
:: deftheorem Def3 defines RealLinearSpace-yielding PRVECT_2:def 3 :
for R being Relation holds
( R is RealLinearSpace-yielding iff for S being set st S in rng R holds
S is RealLinearSpace );
:: deftheorem Def4 defines carr PRVECT_2:def 4 :
for G being RealLinearSpace-Sequence
for b2 being Domain-Sequence holds
( b2 = carr G iff ( len b2 = len G & ( for j being Element of dom G holds b2 . j = the carrier of (G . j) ) ) );
:: deftheorem Def5 defines addop PRVECT_2:def 5 :
for G being RealLinearSpace-Sequence
for b2 being BinOps of carr G holds
( b2 = addop G iff ( len b2 = len (carr G) & ( for j being Element of dom (carr G) holds b2 . j = the addF of (G . j) ) ) );
:: deftheorem Def6 defines complop PRVECT_2:def 6 :
for G being RealLinearSpace-Sequence
for b2 being UnOps of carr G holds
( b2 = complop G iff ( len b2 = len (carr G) & ( for j being Element of dom (carr G) holds b2 . j = comp (G . j) ) ) );
:: deftheorem Def7 defines zeros PRVECT_2:def 7 :
for G being RealLinearSpace-Sequence
for b2 being Element of product (carr G) holds
( b2 = zeros G iff for j being Element of dom (carr G) holds b2 . j = the ZeroF of (G . j) );
:: deftheorem Def8 defines multop PRVECT_2:def 8 :
for G being RealLinearSpace-Sequence
for b2 being MultOps of REAL , carr G holds
( b2 = multop G iff ( len b2 = len (carr G) & ( for j being Element of dom (carr G) holds b2 . j = the Mult of (G . j) ) ) );
:: deftheorem defines product PRVECT_2:def 9 :
for G being RealLinearSpace-Sequence holds product G = RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #);
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 (G . i) 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 (G . i) st vi = v . i holds
([:(multop G):] . r,v) . i = r * vi ) )
Lm5:
for G being RealLinearSpace-Sequence holds
( product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital )
begin
:: deftheorem Def10 defines RealNormSpace-yielding PRVECT_2:def 10 :
for R being Relation holds
( R is RealNormSpace-yielding iff for x being set st x in rng R holds
x is RealNormSpace );
Lm6:
for g being RealNormSpace-yielding FinSequence holds g is RealLinearSpace-yielding
:: deftheorem Def11 defines normsequence PRVECT_2:def 11 :
for G being RealNormSpace-Sequence
for x being Element of product (carr G)
for b3 being Element of REAL (len G) holds
( b3 = normsequence G,x iff ( len b3 = len G & ( for j being Element of dom G holds b3 . j = the normF of (G . j) . (x . j) ) ) );
:: deftheorem Def12 defines productnorm PRVECT_2:def 12 :
for G being RealNormSpace-Sequence
for b2 being Function of (product (carr G)),REAL holds
( b2 = productnorm G iff for x being Element of product (carr G) holds b2 . x = |.(normsequence G,x).| );
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
normF 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 normF 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 normF of b1 = productnorm G & RLSStruct(# the carrier of b2,the ZeroF of b2,the addF of b2,the Mult of b2 #) = product G & the normF of b2 = productnorm G holds
b1 = b2
;
end;
:: deftheorem Def13 defines product PRVECT_2:def 13 :
for G being RealNormSpace-Sequence
for b2 being non empty strict NORMSTR holds
( b2 = product G iff ( RLSStruct(# the carrier of b2,the ZeroF of b2,the addF of b2,the Mult of b2 #) = product G & the normF of b2 = productnorm G ) );
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
Lm7:
for G being RealNormSpace-Sequence holds
( product G is reflexive & product G is discerning & product G is RealNormSpace-like )
theorem Th10:
Lm8:
for RNS being RealNormSpace
for S being sequence of RNS
for g being Point of RNS holds
( S is convergent & lim S = g iff ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) )
theorem Th11:
theorem
theorem Th13:
theorem