let V be RealLinearSpace; 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; 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; ( 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
; (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; XBOOLE_0:def 10 (conv A) /\ (conv B) c= (conv (A \ {v})) /\ (conv B)
let x be object ; TARSKI:def 3 ( not x in (conv A) /\ (conv B) or x in (conv (A \ {v})) /\ (conv B) )
assume A5:
x in (conv A) /\ (conv B)
; 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;