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
proof
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;
sum (x |-- I) = 1 by A1, Def7;
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