let x be set ; :: thesis: for V being RealLinearSpace

for I being affinely-independent Subset of V st x in Affin I & ( for v being VECTOR of V st v in I holds

0 <= (x |-- I) . v ) holds

x in conv I

let V be RealLinearSpace; :: thesis: for I being affinely-independent Subset of V st x in Affin I & ( for v being VECTOR of V st v in I holds

0 <= (x |-- I) . v ) holds

x in conv I

let I be affinely-independent Subset of V; :: thesis: ( x in Affin I & ( for v being VECTOR of V st v in I holds

0 <= (x |-- I) . v ) implies x in conv I )

assume that

A1: x in Affin I and

A2: for v being VECTOR of V st v in I holds

0 <= (x |-- I) . v ; :: thesis: x in conv I

set xI = x |-- I;

A3: Sum (x |-- I) = x by A1, Def7;

reconsider I1 = I as non empty Subset of V by A1;

A4: for v being VECTOR of V holds 0 <= (x |-- I) . v

then A6: x |-- I is convex by A4, Th62;

then ( conv I1 = { (Sum L) where L is Convex_Combination of I1 : L in ConvexComb V } & x |-- I in ConvexComb V ) by CONVEX3:5, CONVEX3:def 1;

hence x in conv I by A3, A6; :: thesis: verum

for I being affinely-independent Subset of V st x in Affin I & ( for v being VECTOR of V st v in I holds

0 <= (x |-- I) . v ) holds

x in conv I

let V be RealLinearSpace; :: thesis: for I being affinely-independent Subset of V st x in Affin I & ( for v being VECTOR of V st v in I holds

0 <= (x |-- I) . v ) holds

x in conv I

let I be affinely-independent Subset of V; :: thesis: ( x in Affin I & ( for v being VECTOR of V st v in I holds

0 <= (x |-- I) . v ) implies x in conv I )

assume that

A1: x in Affin I and

A2: for v being VECTOR of V st v in I holds

0 <= (x |-- I) . v ; :: thesis: x in conv I

set xI = x |-- I;

A3: Sum (x |-- I) = x by A1, Def7;

reconsider I1 = I as non empty Subset of V by A1;

A4: for v being VECTOR of V holds 0 <= (x |-- I) . v

proof

sum (x |-- I) = 1
by A1, Def7;
let v be VECTOR of V; :: thesis: 0 <= (x |-- I) . v

A5: ( v in Carrier (x |-- I) or not v in Carrier (x |-- I) ) ;

Carrier (x |-- I) c= I by RLVECT_2:def 6;

hence 0 <= (x |-- I) . v by A2, A5; :: thesis: verum

end;A5: ( v in Carrier (x |-- I) or not v in Carrier (x |-- I) ) ;

Carrier (x |-- I) c= I by RLVECT_2:def 6;

hence 0 <= (x |-- I) . v by A2, A5; :: thesis: verum

then A6: x |-- I is convex by A4, Th62;

then ( conv I1 = { (Sum L) where L is Convex_Combination of I1 : L in ConvexComb V } & x |-- I in ConvexComb V ) by CONVEX3:5, CONVEX3:def 1;

hence x in conv I by A3, A6; :: thesis: verum