let V be RealLinearSpace; :: thesis: for A being Subset of V
for L being Linear_Combination of A st L is convex & Sum L in Int A holds
Carrier L = A
let A be Subset of V; :: thesis: for L being Linear_Combination of A st L is convex & Sum L in Int A holds
Carrier L = A
let L be Linear_Combination of A; :: thesis: ( L is convex & Sum L in Int A implies Carrier L = A )
assume that
A1: L is convex and
A2: Sum L in Int A ; :: thesis: Carrier L = A
reconsider C = Carrier L as non empty Subset of V by A1, CONVEX1:21;
reconsider LC = L as Linear_Combination of C by RLVECT_2:def 6;
LC in ConvexComb V by A1, CONVEX3:def 1;
then Sum LC in { (Sum M) where M is Convex_Combination of C : M in ConvexComb V } by A1;
then A3: Sum L in conv C by CONVEX3:5;
A4: Carrier L c= A by RLVECT_2:def 6;
assume Carrier L <> A ; :: thesis: contradiction
then Carrier L c< A by A4;
hence contradiction by A2, A3, Def1; :: thesis: verum