environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, RLVECT_1, SUBSET_1, REAL_1, RELAT_1, CARD_1, ARYTM_3, ARYTM_1, TARSKI, SUPINF_2, ALGSTR_0, RUSUB_4, RLSUB_1, STRUCT_0, XXREAL_0, SETFAM_1, BHSP_1, PROB_2, RLVECT_2, FINSEQ_1, FUNCT_1, CARD_3, NAT_1, PARTFUN1, VALUED_1, CONVEX1;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, DOMAIN_1, STRUCT_0, ALGSTR_0, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, FUNCT_1, NAT_1, REAL_1, PARTFUN1, FINSEQ_1, RLVECT_1, RLSUB_1, RLVECT_2, RVSUM_1, BHSP_1, RUSUB_4, RUSUB_5, XXREAL_0;
definitions TARSKI, XBOOLE_0;
theorems BHSP_1, RLVECT_1, RVSUM_1, FUNCT_1, FINSEQ_1, TARSKI, ZFMISC_1, XBOOLE_0, SETFAM_1, RLSUB_1, RUSUB_4, RUSUB_5, RLVECT_2, CARD_1, FINSEQ_3, FINSEQ_4, CARD_2, ENUMSET1, XCMPLX_1, XREAL_1, FINSOP_1, PARTFUN1;
schemes DOMAIN_1, SUBSET_1;
registrations SUBSET_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, STRUCT_0, RLVECT_1, RUSUB_4, VALUED_0, FINSEQ_1, CARD_1, ORDINAL1;
constructors HIDDEN, SETFAM_1, DOMAIN_1, XXREAL_0, REAL_1, PARTFUN1, BINOP_2, FINSEQ_4, FINSOP_1, RVSUM_1, RLVECT_2, RUSUB_5, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, RLVECT_1, RVSUM_1;
expansions TARSKI, XBOOLE_0;
Lm1:
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V holds 1 * M = M
Lm2:
for V being RealLinearSpace
for M being non empty Subset of V holds 0 * M = {(0. V)}
Lm3:
for V being non empty add-associative addLoopStr
for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3)
Lm4:
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V
for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M
Lm5:
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M1, M2 being Subset of V
for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2)
Lm6:
for V being non empty RLSStruct
for M, N being Subset of V
for r being Real st M c= N holds
r * M c= r * N
Lm7:
for V being non empty RLSStruct
for M being empty Subset of V
for r being Real holds r * M = {}
Lm8:
for V being non empty addLoopStr
for M being empty Subset of V
for N being Subset of V holds M + N = {}
Lm9:
for V being non empty right_zeroed addLoopStr
for M being Subset of V holds M + {(0. V)} = M
Lm10:
for V being RealLinearSpace
for M being Subset of V
for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds
(r1 * M) + (r2 * M) c= (r1 + r2) * M
Lm11:
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V st L is convex & Carrier L = {v} holds
( L . v = 1 & Sum L = (L . v) * v )
Lm12:
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for L being Linear_Combination of V st L is convex & Carrier L = {v1,v2} & v1 <> v2 holds
( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
Lm13:
for p being FinSequence
for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> holds
p = <*z,y,x*>
Lm14:
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for L being Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 holds
Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
Lm15:
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for L being Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds
( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
theorem
for
p being
FinSequence for
x,
y,
z being
set st
p is
one-to-one &
rng p = {x,y,z} &
x <> y &
y <> z &
z <> x & not
p = <*x,y,z*> & not
p = <*x,z,y*> & not
p = <*y,x,z*> & not
p = <*y,z,x*> & not
p = <*z,x,y*> holds
p = <*z,y,x*> by Lm13;