environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, RLVECT_1, BINOP_1, ZFMISC_1, STRUCT_0, SUBSET_1, FUNCT_1, ALGSTR_0, REAL_1, SUPINF_2, RELAT_1, ARYTM_3, FINSEQ_1, CARD_3, CARD_1, XXREAL_0, TARSKI, PARTFUN1, ORDINAL4, BINOP_2, ARYTM_1, SUPINF_1, NAT_1, FUNCT_2, RFINSEQ, CONVEX1, RFUNCT_3, FINSET_1, CLASSES1, CONVFUN1, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0, XXREAL_3, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, SUPINF_1, ZFMISC_1, MEASURE6, BINOP_1, FUNCT_2, SUPINF_2, DOMAIN_1, BINOP_2, FINSET_1, CLASSES1, RFINSEQ, RFUNCT_3, NAT_1, RVSUM_1, EXTREAL1, FINSEQ_1, FINSEQ_4, STRUCT_0, ALGSTR_0, RLVECT_1, CONVEX1;
definitions RLVECT_1, ALGSTR_0;
theorems ZFMISC_1, FUNCT_2, CONVEX1, SUPINF_2, EXTREAL1, RLVECT_1, RFUNCT_3, RVSUM_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_5, NAT_1, TARSKI, FUNCT_1, CARD_2, INT_1, XCMPLX_1, XBOOLE_0, RFINSEQ, RLVECT_2, RELAT_1, XBOOLE_1, BINOP_2, XREAL_1, XXREAL_0, XREAL_0, FINSOP_1, PARTFUN1, ALGSTR_0, VALUED_1, XXREAL_3, XTUPLE_0;
schemes BINOP_1, DOMAIN_1, FINSEQ_2, FRAENKEL, NAT_1, RECDEF_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, STRUCT_0, RLVECT_1, VALUED_0, ALGSTR_0, CARD_1, XXREAL_3, INT_1, ORDINAL1;
constructors HIDDEN, BINOP_1, DOMAIN_1, REAL_1, FINSEQ_4, FINSOP_1, RVSUM_1, SUPINF_2, RFINSEQ, RFUNCT_3, MEASURE6, EXTREAL1, CONVEX1, BINOP_2, SUPINF_1, CLASSES1, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities BINOP_1, RLVECT_1, RVSUM_1, STRUCT_0, ALGSTR_0;
expansions BINOP_1, RLVECT_1;
definition
let X,
Y be non
empty RLSStruct ;
func Add_in_Prod_of_RLS (
X,
Y)
-> BinOp of
[: the carrier of X, the carrier of Y:] means :
Def1:
for
z1,
z2 being
Element of
[: the carrier of X, the carrier of Y:] for
x1,
x2 being
VECTOR of
X for
y1,
y2 being
VECTOR of
Y st
z1 = [x1,y1] &
z2 = [x2,y2] holds
it . (
z1,
z2)
= [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])];
existence
ex b1 being BinOp of [: the carrier of X, the carrier of Y:] st
for z1, z2 being Element of [: the carrier of X, the carrier of Y:]
for x1, x2 being VECTOR of X
for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds
b1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])]
uniqueness
for b1, b2 being BinOp of [: the carrier of X, the carrier of Y:] st ( for z1, z2 being Element of [: the carrier of X, the carrier of Y:]
for x1, x2 being VECTOR of X
for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds
b1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) & ( for z1, z2 being Element of [: the carrier of X, the carrier of Y:]
for x1, x2 being VECTOR of X
for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds
b2 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) holds
b1 = b2
end;
::
deftheorem Def1 defines
Add_in_Prod_of_RLS CONVFUN1:def 1 :
for X, Y being non empty RLSStruct
for b3 being BinOp of [: the carrier of X, the carrier of Y:] holds
( b3 = Add_in_Prod_of_RLS (X,Y) iff for z1, z2 being Element of [: the carrier of X, the carrier of Y:]
for x1, x2 being VECTOR of X
for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds
b3 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] );
definition
let X,
Y be non
empty RLSStruct ;
func Mult_in_Prod_of_RLS (
X,
Y)
-> Function of
[:REAL,[: the carrier of X, the carrier of Y:]:],
[: the carrier of X, the carrier of Y:] means :
Def2:
for
a being
Real for
z being
Element of
[: the carrier of X, the carrier of Y:] for
x being
VECTOR of
X for
y being
VECTOR of
Y st
z = [x,y] holds
it . (
a,
z)
= [( the Mult of X . [a,x]),( the Mult of Y . [a,y])];
existence
ex b1 being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] st
for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
b1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])]
uniqueness
for b1, b2 being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] st ( for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
b1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) & ( for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
b2 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) holds
b1 = b2
end;
::
deftheorem Def2 defines
Mult_in_Prod_of_RLS CONVFUN1:def 2 :
for X, Y being non empty RLSStruct
for b3 being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] holds
( b3 = Mult_in_Prod_of_RLS (X,Y) iff for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
b3 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] );
Lm1:
for X being non empty RLSStruct
for x being VECTOR of X
for u being VECTOR of (Prod_of_RLS (X,RLS_Real))
for p, w being Real st u = [x,w] holds
p * u = [(p * x),(p * w)]
Lm2:
for X being non empty RLSStruct
for x1, x2 being VECTOR of X
for w1, w2 being Real
for u1, u2 being VECTOR of (Prod_of_RLS (X,RLS_Real)) st u1 = [x1,w1] & u2 = [x2,w2] holds
u1 + u2 = [(x1 + x2),(w1 + w2)]
Lm3:
for a being FinSequence of the carrier of RLS_Real
for b being FinSequence of REAL st len a = len b & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b
Lm4:
for F being FinSequence of ExtREAL
for x being Element of ExtREAL holds Sum (F ^ <*x*>) = (Sum F) + x
Lm5:
for F being FinSequence of ExtREAL st not -infty in rng F holds
Sum F <> -infty
Lm6:
for F being FinSequence of ExtREAL st +infty in rng F & not -infty in rng F holds
Sum F = +infty
Lm7:
for a being FinSequence of ExtREAL
for b being FinSequence of REAL st len a = len b & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b
Lm8:
for n being Element of NAT
for a being FinSequence of ExtREAL
for b being FinSequence of the carrier of RLS_Real st len a = n & len b = n & ( for i being Element of NAT st i in Seg n holds
a . i = b . i ) holds
Sum a = Sum b
Lm9:
for F being FinSequence of ExtREAL st rng F c= {0.} holds
Sum F = 0.
Lm10:
for F being FinSequence of REAL st rng F c= {0} holds
Sum F = 0
Lm11:
for X being RealLinearSpace
for F being FinSequence of the carrier of X st rng F c= {(0. X)} holds
Sum F = 0. X
Lm12:
for w1, w2 being R_eal
for wr1, wr2, p1, p2 being Real st w1 = wr1 & w2 = wr2 holds
(p1 * wr1) + (p2 * wr2) = (p1 * w1) + (p2 * w2)
Lm13:
for X being RealLinearSpace
for f being Function of the carrier of X,ExtREAL
for n being non zero Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y being FinSequence of the carrier of X st len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (p . i) * (f . (y /. i)) ) ) holds
not -infty in rng F
Lm14:
for F being FinSequence of REAL ex s being Permutation of (dom F) ex n being Element of NAT st
for i being Element of NAT st i in dom F holds
( i in Seg n iff F . (s . i) <> 0 )