let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for A, B, Aff being Subset of V st Aff is Affine & (conv A) /\ (conv B) c= Aff & conv (A \ {v}) c= Aff & not v in Aff holds
(conv (A \ {v})) /\ (conv B) = (conv A) /\ (conv B)
let v be VECTOR of V; :: thesis: for A, B, Aff being Subset of V st Aff is Affine & (conv A) /\ (conv B) c= Aff & conv (A \ {v}) c= Aff & not v in Aff holds
(conv (A \ {v})) /\ (conv B) = (conv A) /\ (conv B)
let A, B, Aff be Subset of V; :: thesis: ( Aff is Affine & (conv A) /\ (conv B) c= Aff & conv (A \ {v}) c= Aff & not v in Aff implies (conv (A \ {v})) /\ (conv B) = (conv A) /\ (conv B) )
assume that
A1: Aff is Affine and
A2: (conv A) /\ (conv B) c= Aff and
A3: conv (A \ {v}) c= Aff and
A4: not v in Aff ; :: thesis: (conv (A \ {v})) /\ (conv B) = (conv A) /\ (conv B)
conv (A \ {v}) c= conv A by RLTOPSP1:20, XBOOLE_1:36;
hence (conv (A \ {v})) /\ (conv B) c= (conv A) /\ (conv B) by XBOOLE_1:26; :: according to XBOOLE_0:def 10 :: thesis: (conv A) /\ (conv B) c= (conv (A \ {v})) /\ (conv B)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (conv A) /\ (conv B) or x in (conv (A \ {v})) /\ (conv B) )
assume A5: x in (conv A) /\ (conv B) ; :: thesis: x in (conv (A \ {v})) /\ (conv B)
then reconsider A1 = A as non empty Subset of V by XBOOLE_0:def 4;
A6: x in Aff by A2, A5;
( conv A = { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } & x in conv A ) by A5, CONVEX3:5, XBOOLE_0:def 4;
then consider L being Convex_Combination of A1 such that
A7: x = Sum L and
L in ConvexComb V ;
set Lv = L . v;
A8: Carrier L c= A by RLVECT_2:def 6;
A9: x in conv B by A5, XBOOLE_0:def 4;
per cases ( L . v = 0 or L . v <> 0 ) ;
suppose L . v = 0 ; :: thesis: x in (conv (A \ {v})) /\ (conv B)
then not v in Carrier L by RLVECT_2:19;
then A10: Carrier L c= A \ {v} by A8, ZFMISC_1:34;
then reconsider K = L as Linear_Combination of A \ {v} by RLVECT_2:def 6;
Carrier L <> {} by CONVEX1:21;
then reconsider Av = A \ {v} as non empty Subset of V by A10;
K in ConvexComb V by CONVEX3:def 1;
then Sum K in { (Sum M) where M is Convex_Combination of Av : M in ConvexComb V } ;
then x in conv Av by A7, CONVEX3:5;
hence x in (conv (A \ {v})) /\ (conv B) by A9, XBOOLE_0:def 4; :: thesis: verum
end;
suppose L . v <> 0 ; :: thesis: x in (conv (A \ {v})) /\ (conv B)
then ex p being Element of V st
( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v ) by A4, A6, A7, Th1;
hence x in (conv (A \ {v})) /\ (conv B) by A1, A2, A3, A4, A5, A7, RUSUB_4:def 4; :: thesis: verum
end;
end;