let x be set ; :: thesis: for V being RealLinearSpace
for v being VECTOR of V
for I being affinely-independent Subset of V st x in conv I holds
( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )
let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for I being affinely-independent Subset of V st x in conv I holds
( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )
let v be VECTOR of V; :: thesis: for I being affinely-independent Subset of V st x in conv I holds
( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )
let I be affinely-independent Subset of V; :: thesis: ( x in conv I implies ( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 ) )
assume A1: x in conv I ; :: thesis: ( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )
then reconsider I1 = I as non empty Subset of V ;
conv I1 = { (Sum L) where L is Convex_Combination of I1 : L in ConvexComb V } by CONVEX3:5;
then consider L being Convex_Combination of I1 such that
A2: Sum L = x and
L in ConvexComb V by A1;
( conv I c= Affin I & sum L = 1 ) by Th62, Th65;
then L = x |-- I by A1, A2, Def7;
hence ( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 ) by Th62, Th63; :: thesis: verum