let x be set ; :: thesis: for V being RealLinearSpace
for A being Subset of V st x in Int A holds
ex L being Linear_Combination of A st
( L is convex & x = Sum L )
let V be RealLinearSpace; :: thesis: for A being Subset of V st x in Int A holds
ex L being Linear_Combination of A st
( L is convex & x = Sum L )
let A be Subset of V; :: thesis: ( x in Int A implies ex L being Linear_Combination of A st
( L is convex & x = Sum L ) )
assume A1: x in Int A ; :: thesis: ex L being Linear_Combination of A st
( L is convex & x = Sum L )
then reconsider A1 = A as non empty Subset of V ;
x in conv A by A1, Def1;
then x in { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5;
then ex L being Convex_Combination of A1 st
( x = Sum L & L in ConvexComb V ) ;
hence ex L being Linear_Combination of A st
( L is convex & x = Sum L ) ; :: thesis: verum