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

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