environ
vocabularies HIDDEN, NUMBERS, RLVECT_1, CONVEX2, FUNCT_2, STRUCT_0, XBOOLE_0, SUBSET_1, CARD_3, RLVECT_2, FUNCT_1, FINSEQ_1, RELAT_1, VALUED_1, TARSKI, NAT_1, XXREAL_0, CARD_1, ARYTM_3, ORDINAL4, CONVEX1, REAL_1, ARYTM_1, RFINSEQ, PARTFUN1, FINSET_1, SUPINF_2, CONVEX3, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, XCMPLX_0, XREAL_0, XXREAL_0, REAL_1, RELAT_1, FUNCT_1, FINSET_1, ORDINAL1, DOMAIN_1, PARTFUN1, NUMBERS, STRUCT_0, ALGSTR_0, FUNCT_2, FINSEQ_1, RLVECT_1, RLVECT_2, RVSUM_1, CONVEX1, RFINSEQ, CONVEX2;
definitions TARSKI;
theorems RLVECT_1, RVSUM_1, FUNCT_1, FINSEQ_1, TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1, RLVECT_2, CARD_1, FINSEQ_3, FINSEQ_4, ENUMSET1, CONVEX1, FUNCT_2, NAT_1, RFINSEQ, CONVEX2, RLVECT_3, CARD_2, FINSEQ_5, PARTFUN2, GRAPH_5, RELAT_1, XCMPLX_1, XREAL_1, XXREAL_0, FINSOP_1, ORDINAL1, PARTFUN1, VALUED_1, RLVECT_4, XREAL_0;
schemes NAT_1, XBOOLE_0, FINSEQ_1, CLASSES1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, STRUCT_0, RLVECT_1, VALUED_0, CARD_1, RLVECT_2;
constructors HIDDEN, DOMAIN_1, REAL_1, FINSOP_1, RVSUM_1, RFINSEQ, CONVEX1, BINOP_2, RELSET_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities RVSUM_1;
expansions TARSKI;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
reconsider jd = 1 / 2, jt = 1 / 3 as Element of REAL by XREAL_0:def 1;
Lm1:
for V being RealLinearSpace
for M being non empty Subset of V st { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M holds
M is convex
Lm2:
for V being RealLinearSpace
for M being non empty Subset of V
for L being Convex_Combination of M st card (Carrier L) >= 2 holds
ex L1, L2 being Convex_Combination of M ex r being Real st
( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 )
Lm3:
for V being RealLinearSpace
for M being non empty Subset of V st M is convex holds
{ (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M
Lm4:
for V being RealLinearSpace
for M being Subset of V
for L being Linear_Combination of M st card (Carrier L) >= 1 holds
ex L1, L2 being Linear_Combination of M st
( Sum L = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 & Carrier L1 c= Carrier L & Carrier L2 c= Carrier L & ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = L . v ) & ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = L . v ) )