let x be set ; :: thesis: for V being RealLinearSpace
for I being affinely-independent Subset of V
for B being Subset of V st x in conv I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
x in conv (I \ B)
let V be RealLinearSpace; :: thesis: for I being affinely-independent Subset of V
for B being Subset of V st x in conv I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
x in conv (I \ B)
let I be affinely-independent Subset of V; :: thesis: for B being Subset of V st x in conv I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
x in conv (I \ B)
let B be Subset of V; :: thesis: ( x in conv I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) implies x in conv (I \ B) )
assume that
A1: x in conv I and
A2: for y being set st y in B holds
(x |-- I) . y = 0 ; :: thesis: x in conv (I \ B)
set IB = I \ B;
A3: conv I c= Affin I by Th65;
then x |-- I = x |-- (I \ B) by A1, A2, Th75;
then A4: for v being VECTOR of V st v in I \ B holds
0 <= (x |-- (I \ B)) . v by A1, Th71;
A5: I \ B is affinely-independent by Th43, XBOOLE_1:36;
x in Affin (I \ B) by A1, A2, A3, Th75;
hence x in conv (I \ B) by A4, A5, Th73; :: thesis: verum