environ
vocabularies HIDDEN, NUMBERS, REAL_1, FINSEQ_1, XBOOLE_0, RLVECT_1, CONVEX1, SUBSET_1, BHSP_1, STRUCT_0, RELAT_1, FUNCT_1, PROB_2, XXREAL_0, CARD_1, ARYTM_3, ARYTM_1, RLVECT_2, TARSKI, CARD_3, NAT_1, VALUED_1, JORDAN3, PARTFUN1, ORDINAL4, FUNCT_2, RLSUB_1, RUSUB_4, CLASSES1, FINSET_1, CONVEX2, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, NAT_1, FINSEQ_1, DOMAIN_1, STRUCT_0, ALGSTR_0, RLVECT_1, RLSUB_1, RLSUB_2, FINSEQ_4, RLVECT_2, RVSUM_1, BHSP_1, RUSUB_4, CONVEX1, FINSEQ_6, CLASSES1;
definitions TARSKI, CONVEX1;
theorems BHSP_1, RLVECT_1, RVSUM_1, FUNCT_1, FINSEQ_1, TARSKI, ZFMISC_1, XBOOLE_0, RUSUB_4, XBOOLE_1, RLVECT_2, CARD_1, FINSEQ_3, FINSEQ_4, ENUMSET1, CONVEX1, PARTFUN1, FINSEQ_6, RLSUB_2, FUNCT_2, NAT_1, FVSUM_1, RFINSEQ, FINSET_1, INTEGRA5, XCMPLX_1, XREAL_1, XXREAL_0, FINSOP_1, STRUCT_0, VALUED_1, CLASSES1, RLVECT_4, XREAL_0;
schemes NAT_1, XBOOLE_0, FINSEQ_1, CLASSES1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, NUMBERS, XXREAL_0, NAT_1, FINSEQ_1, STRUCT_0, RLVECT_1, RUSUB_4, CONVEX1, VALUED_0, RELSET_1, RLVECT_2, XREAL_0, ORDINAL1, RVSUM_1, CARD_1;
constructors HIDDEN, WELLORD2, DOMAIN_1, REAL_1, BINOP_2, FINSEQ_4, FINSOP_1, RLSUB_2, RUSUB_4, CONVEX1, MATRIX_1, FINSEQ_6, RVSUM_1, CLASSES1, RELSET_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities FINSEQ_1, RVSUM_1;
expansions TARSKI, CONVEX1;
reconsider rr = 1 as Element of REAL by XREAL_0:def 1;
set ff = <*rr*>;
Lm1:
for V being RealLinearSpace
for M being convex Subset of V
for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
Lm2:
for V being RealLinearSpace
for M being Subset of V st ( for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ) holds
M is convex
Lm3:
for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 + W2) = (Up W1) + (Up W2)
Lm4:
for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2)
Lm5:
for V being RealLinearSpace
for L1, L2 being Convex_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
Lm6:
for F, G being Function st F,G are_fiberwise_equipotent holds
for x1, x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex z1, z2 being set st
( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 )
Lm7:
for V being RealLinearSpace
for L being Linear_Combination of V
for A being Subset of V st A c= Carrier L holds
ex L1 being Linear_Combination of V st Carrier L1 = A