let x be set ; :: thesis: for V being RealLinearSpace
for I being affinely-independent Subset of V st x in I holds
(conv I) \ {x} is convex
let V be RealLinearSpace; :: thesis: for I being affinely-independent Subset of V st x in I holds
(conv I) \ {x} is convex
let I be affinely-independent Subset of V; :: thesis: ( x in I implies (conv I) \ {x} is convex )
assume A1: x in I ; :: thesis: (conv I) \ {x} is convex
then reconsider X = x as Element of V ;
A2: conv I c= Affin I by Th65;
now :: thesis: for v1, v2 being VECTOR of V
for r being Real st 0 < r & r < 1 & v1 in (conv I) \ {x} & v2 in (conv I) \ {x} holds
(r * v1) + ((1 - r) * v2) in (conv I) \ {x}
let v1, v2 be VECTOR of V; :: thesis: for r being Real st 0 < r & r < 1 & v1 in (conv I) \ {x} & v2 in (conv I) \ {x} holds
(r * v1) + ((1 - r) * v2) in (conv I) \ {x}
let r be Real; :: thesis: ( 0 < r & r < 1 & v1 in (conv I) \ {x} & v2 in (conv I) \ {x} implies (r * v1) + ((1 - r) * v2) in (conv I) \ {x} )
set rv12 = (r * v1) + ((1 - r) * v2);
assume that
A3: 0 < r and
A4: r < 1 ; :: thesis: ( v1 in (conv I) \ {x} & v2 in (conv I) \ {x} implies (r * v1) + ((1 - r) * v2) in (conv I) \ {x} )
assume that
A5: v1 in (conv I) \ {x} and
A6: v2 in (conv I) \ {x} ; :: thesis: (r * v1) + ((1 - r) * v2) in (conv I) \ {x}
A7: 1 - r > 1 - 1 by A4, XREAL_1:10;
A8: v2 in conv I by A6, ZFMISC_1:56;
then A9: (v2 |-- I) . X <= 1 by Th71;
A10: v1 in conv I by A5, ZFMISC_1:56;
then A11: (v1 |-- I) . X <= 1 by Th71;
A12: ((r * v1) + ((1 - r) * v2)) |-- I = ((1 - r) * (v2 |-- I)) + (r * (v1 |-- I)) by A2, A10, A8, Th70;
A13: now :: thesis: for w being VECTOR of V st w in I holds
0 <= (((r * v1) + ((1 - r) * v2)) |-- I) . w
let w be VECTOR of V; :: thesis: ( w in I implies 0 <= (((r * v1) + ((1 - r) * v2)) |-- I) . w )
assume w in I ; :: thesis: 0 <= (((r * v1) + ((1 - r) * v2)) |-- I) . w
A14: (((r * v1) + ((1 - r) * v2)) |-- I) . w = (((1 - r) * (v2 |-- I)) . w) + ((r * (v1 |-- I)) . w) by A12, RLVECT_2:def 10
.= ((1 - r) * ((v2 |-- I) . w)) + ((r * (v1 |-- I)) . w) by RLVECT_2:def 11
.= ((1 - r) * ((v2 |-- I) . w)) + (r * ((v1 |-- I) . w)) by RLVECT_2:def 11 ;
( (v2 |-- I) . w >= 0 & (v1 |-- I) . w >= 0 ) by A10, A8, Th71;
hence 0 <= (((r * v1) + ((1 - r) * v2)) |-- I) . w by A3, A7, A14; :: thesis: verum
end;
(r * v1) + ((1 - r) * v2) in Affin I by A2, A10, A8, RUSUB_4:def 4;
then A15: (r * v1) + ((1 - r) * v2) in conv I by A13, Th73;
v1 <> x by A5, ZFMISC_1:56;
then (v1 |-- I) . X <> 1 by A10, Th72;
then (v1 |-- I) . X < 1 by A11, XXREAL_0:1;
then A16: r * ((v1 |-- I) . X) < r * 1 by A3, XREAL_1:68;
v2 <> x by A6, ZFMISC_1:56;
then (v2 |-- I) . X <> 1 by A8, Th72;
then (v2 |-- I) . X < 1 by A9, XXREAL_0:1;
then (1 - r) * ((v2 |-- I) . X) < (1 - r) * 1 by A7, XREAL_1:68;
then A17: ((1 - r) * ((v2 |-- I) . X)) + (r * ((v1 |-- I) . X)) < ((1 - r) * 1) + (r * 1) by A16, XREAL_1:8;
(((r * v1) + ((1 - r) * v2)) |-- I) . X = (((1 - r) * (v2 |-- I)) . X) + ((r * (v1 |-- I)) . X) by A12, RLVECT_2:def 10
.= ((1 - r) * ((v2 |-- I) . X)) + ((r * (v1 |-- I)) . X) by RLVECT_2:def 11
.= ((1 - r) * ((v2 |-- I) . X)) + (r * ((v1 |-- I) . X)) by RLVECT_2:def 11 ;
then (r * v1) + ((1 - r) * v2) <> X by A1, A15, A17, Th72;
hence (r * v1) + ((1 - r) * v2) in (conv I) \ {x} by A15, ZFMISC_1:56; :: thesis: verum
end;
hence (conv I) \ {x} is convex ; :: thesis: verum