let x be set ; :: thesis: for V being RealLinearSpace

for A being Subset of V st x in conv A & (conv A) \ {x} is convex holds

x in A

let V be RealLinearSpace; :: thesis: for A being Subset of V st x in conv A & (conv A) \ {x} is convex holds

x in A

let A be Subset of V; :: thesis: ( x in conv A & (conv A) \ {x} is convex implies x in A )

assume that

A1: x in conv A and

A2: (conv A) \ {x} is convex ; :: thesis: x in A

reconsider A1 = A as non empty Subset of V by A1;

A3: conv A1 = { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5;

assume A4: not x in A ; :: thesis: contradiction

consider L being Convex_Combination of A1 such that

A5: Sum L = x and

L in ConvexComb V by A1, A3;

set C = Carrier L;

A6: Carrier L c= A1 by RLVECT_2:def 6;

Carrier L <> {} by CONVEX1:21;

then consider p being object such that

A7: p in Carrier L by XBOOLE_0:def 1;

reconsider p = p as Element of V by A7;

A8: sum L = 1 by Th62;

(Carrier L) \ {p} <> {}

A11: q in (Carrier L) \ {p} by XBOOLE_0:def 1;

reconsider q = q as Element of V by A11;

A12: q in Carrier L by A11, XBOOLE_0:def 5;

then L . q <> 0 by RLVECT_2:19;

then A13: L . q > 0 by Th62;

reconsider mm = min ((L . p),(L . q)) as Real ;

consider Lq being Linear_Combination of {q} such that

A14: Lq . q = mm by RLVECT_4:37;

A15: p <> q by A11, ZFMISC_1:56;

then A16: p - q <> 0. V by RLVECT_1:21;

A17: Carrier Lq c= {q} by RLVECT_2:def 6;

{q} c= A by A6, A12, ZFMISC_1:31;

then Carrier Lq c= A by A17;

then A18: Lq is Linear_Combination of A by RLVECT_2:def 6;

consider Lp being Linear_Combination of {p} such that

A19: Lp . p = mm by RLVECT_4:37;

A20: Carrier Lp c= {p} by RLVECT_2:def 6;

{p} c= A by A6, A7, ZFMISC_1:31;

then Carrier Lp c= A by A20;

then Lp is Linear_Combination of A by RLVECT_2:def 6;

then A21: Lp - Lq is Linear_Combination of A by A18, RLVECT_2:56;

then - (Lp - Lq) is Linear_Combination of A by RLVECT_2:52;

then reconsider Lpq = L + (Lp - Lq), L1pq = L - (Lp - Lq) as Linear_Combination of A1 by A21, RLVECT_2:38;

A22: Sum L1pq = (Sum L) - (Sum (Lp - Lq)) by RLVECT_3:4

.= (Sum L) + (- (Sum (Lp - Lq))) by RLVECT_1:def 11 ;

L . p <> 0 by A7, RLVECT_2:19;

then L . p > 0 by Th62;

then A23: mm > 0 by A13, XXREAL_0:15;

A24: for v being VECTOR of V holds L1pq . v >= 0

.= (mm * p) - (Sum Lq) by A19, RLVECT_2:32

.= (mm * p) - (mm * q) by A14, RLVECT_2:32

.= mm * (p - q) by RLVECT_1:34 ;

then A32: Sum (Lp - Lq) <> 0. V by A23, A16, RLVECT_1:11;

A33: sum (Lp - Lq) = (sum Lp) - (sum Lq) by Th36

.= mm - (sum Lq) by A19, A20, Th32

.= mm - mm by A14, A17, Th32

.= 0 ;

A34: for v being VECTOR of V holds Lpq . v >= 0

.= 1 + 0 by A33, Th62 ;

then A42: L1pq is convex by A24, Th62;

then L1pq in ConvexComb V by CONVEX3:def 1;

then A43: Sum L1pq in conv A1 by A3, A42;

sum Lpq = (sum L) + (sum (Lp - Lq)) by Th34

.= 1 + 0 by A33, Th62 ;

then A44: Lpq is convex by A34, Th62;

then Lpq in ConvexComb V by CONVEX3:def 1;

then A45: Sum Lpq in conv A by A3, A44;

0. V = - (0. V) ;

then - (Sum (Lp - Lq)) <> 0. V by A32;

then Sum L1pq <> x by A5, A22, RLVECT_1:9;

then A46: Sum L1pq in (conv A) \ {x} by A43, ZFMISC_1:56;

Sum Lpq = (Sum L) + (Sum (Lp - Lq)) by RLVECT_3:1;

then Sum Lpq <> x by A5, A32, RLVECT_1:9;

then A47: Sum Lpq in (conv A) \ {x} by A45, ZFMISC_1:56;

((1 / 2) * (Sum Lpq)) + ((1 - (1 / 2)) * (Sum L1pq)) = ((1 / 2) * ((Sum L) + (Sum (Lp - Lq)))) + ((1 / 2) * ((Sum L) + (- (Sum (Lp - Lq))))) by A22, RLVECT_3:1

.= (((1 / 2) * (Sum L)) + ((1 / 2) * (Sum (Lp - Lq)))) + ((1 / 2) * ((Sum L) + (- (Sum (Lp - Lq))))) by RLVECT_1:def 5

.= (((1 / 2) * (Sum L)) + ((1 / 2) * (Sum (Lp - Lq)))) + (((1 / 2) * (Sum L)) + ((1 / 2) * (- (Sum (Lp - Lq))))) by RLVECT_1:def 5

.= ((1 / 2) * (Sum L)) + (((1 / 2) * (Sum (Lp - Lq))) + (((1 / 2) * (- (Sum (Lp - Lq)))) + ((1 / 2) * (Sum L)))) by RLVECT_1:def 3

.= ((1 / 2) * (Sum L)) + ((((1 / 2) * (Sum (Lp - Lq))) + ((1 / 2) * (- (Sum (Lp - Lq))))) + ((1 / 2) * (Sum L))) by RLVECT_1:def 3

.= ((1 / 2) * (Sum L)) + (((1 / 2) * ((Sum (Lp - Lq)) + (- (Sum (Lp - Lq))))) + ((1 / 2) * (Sum L))) by RLVECT_1:def 5

.= ((1 / 2) * (Sum L)) + (((1 / 2) * (0. V)) + ((1 / 2) * (Sum L))) by RLVECT_1:5

.= ((1 / 2) * (Sum L)) + ((0. V) + ((1 / 2) * (Sum L)))

.= ((1 / 2) * (Sum L)) + ((1 / 2) * (Sum L))

.= ((1 / 2) + (1 / 2)) * (Sum L) by RLVECT_1:def 6

.= Sum L by RLVECT_1:def 8 ;

then Sum L in (conv A) \ {x} by A2, A46, A47;

hence contradiction by A5, ZFMISC_1:56; :: thesis: verum

for A being Subset of V st x in conv A & (conv A) \ {x} is convex holds

x in A

let V be RealLinearSpace; :: thesis: for A being Subset of V st x in conv A & (conv A) \ {x} is convex holds

x in A

let A be Subset of V; :: thesis: ( x in conv A & (conv A) \ {x} is convex implies x in A )

assume that

A1: x in conv A and

A2: (conv A) \ {x} is convex ; :: thesis: x in A

reconsider A1 = A as non empty Subset of V by A1;

A3: conv A1 = { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5;

assume A4: not x in A ; :: thesis: contradiction

consider L being Convex_Combination of A1 such that

A5: Sum L = x and

L in ConvexComb V by A1, A3;

set C = Carrier L;

A6: Carrier L c= A1 by RLVECT_2:def 6;

Carrier L <> {} by CONVEX1:21;

then consider p being object such that

A7: p in Carrier L by XBOOLE_0:def 1;

reconsider p = p as Element of V by A7;

A8: sum L = 1 by Th62;

(Carrier L) \ {p} <> {}

proof

then consider q being object such that
assume A9:
(Carrier L) \ {p} = {}
; :: thesis: contradiction

then Carrier L = {p} by A7, ZFMISC_1:58;

then A10: L . p = 1 by A8, Th32;

Sum L = (L . p) * p by A7, A9, RLVECT_2:35, ZFMISC_1:58;

then x = p by A5, A10, RLVECT_1:def 8;

hence contradiction by A4, A6, A7; :: thesis: verum

end;then Carrier L = {p} by A7, ZFMISC_1:58;

then A10: L . p = 1 by A8, Th32;

Sum L = (L . p) * p by A7, A9, RLVECT_2:35, ZFMISC_1:58;

then x = p by A5, A10, RLVECT_1:def 8;

hence contradiction by A4, A6, A7; :: thesis: verum

A11: q in (Carrier L) \ {p} by XBOOLE_0:def 1;

reconsider q = q as Element of V by A11;

A12: q in Carrier L by A11, XBOOLE_0:def 5;

then L . q <> 0 by RLVECT_2:19;

then A13: L . q > 0 by Th62;

reconsider mm = min ((L . p),(L . q)) as Real ;

consider Lq being Linear_Combination of {q} such that

A14: Lq . q = mm by RLVECT_4:37;

A15: p <> q by A11, ZFMISC_1:56;

then A16: p - q <> 0. V by RLVECT_1:21;

A17: Carrier Lq c= {q} by RLVECT_2:def 6;

{q} c= A by A6, A12, ZFMISC_1:31;

then Carrier Lq c= A by A17;

then A18: Lq is Linear_Combination of A by RLVECT_2:def 6;

consider Lp being Linear_Combination of {p} such that

A19: Lp . p = mm by RLVECT_4:37;

A20: Carrier Lp c= {p} by RLVECT_2:def 6;

{p} c= A by A6, A7, ZFMISC_1:31;

then Carrier Lp c= A by A20;

then Lp is Linear_Combination of A by RLVECT_2:def 6;

then A21: Lp - Lq is Linear_Combination of A by A18, RLVECT_2:56;

then - (Lp - Lq) is Linear_Combination of A by RLVECT_2:52;

then reconsider Lpq = L + (Lp - Lq), L1pq = L - (Lp - Lq) as Linear_Combination of A1 by A21, RLVECT_2:38;

A22: Sum L1pq = (Sum L) - (Sum (Lp - Lq)) by RLVECT_3:4

.= (Sum L) + (- (Sum (Lp - Lq))) by RLVECT_1:def 11 ;

L . p <> 0 by A7, RLVECT_2:19;

then L . p > 0 by Th62;

then A23: mm > 0 by A13, XXREAL_0:15;

A24: for v being VECTOR of V holds L1pq . v >= 0

proof

Sum (Lp - Lq) =
(Sum Lp) - (Sum Lq)
by RLVECT_3:4
let v be VECTOR of V; :: thesis: L1pq . v >= 0

A25: L1pq . v = (L . v) - ((Lp - Lq) . v) by RLVECT_2:54

.= (L . v) - ((Lp . v) - (Lq . v)) by RLVECT_2:54 ;

A26: L . v >= 0 by Th62;

end;A25: L1pq . v = (L . v) - ((Lp - Lq) . v) by RLVECT_2:54

.= (L . v) - ((Lp . v) - (Lq . v)) by RLVECT_2:54 ;

A26: L . v >= 0 by Th62;

per cases
( v = q or v = p or ( v <> p & v <> q ) )
;

end;

suppose A27:
v = q
; :: thesis: L1pq . v >= 0

then
not v in Carrier Lp
by A15, A20, TARSKI:def 1;

then Lp . v = 0 ;

hence L1pq . v >= 0 by A23, A14, A25, A26, A27; :: thesis: verum

end;then Lp . v = 0 ;

hence L1pq . v >= 0 by A23, A14, A25, A26, A27; :: thesis: verum

.= (mm * p) - (Sum Lq) by A19, RLVECT_2:32

.= (mm * p) - (mm * q) by A14, RLVECT_2:32

.= mm * (p - q) by RLVECT_1:34 ;

then A32: Sum (Lp - Lq) <> 0. V by A23, A16, RLVECT_1:11;

A33: sum (Lp - Lq) = (sum Lp) - (sum Lq) by Th36

.= mm - (sum Lq) by A19, A20, Th32

.= mm - mm by A14, A17, Th32

.= 0 ;

A34: for v being VECTOR of V holds Lpq . v >= 0

proof

sum L1pq =
(sum L) - (sum (Lp - Lq))
by Th36
let v be VECTOR of V; :: thesis: Lpq . v >= 0

A35: Lpq . v = (L . v) + ((Lp - Lq) . v) by RLVECT_2:def 10

.= (L . v) + ((Lp . v) - (Lq . v)) by RLVECT_2:54 ;

A36: L . v >= 0 by Th62;

end;A35: Lpq . v = (L . v) + ((Lp - Lq) . v) by RLVECT_2:def 10

.= (L . v) + ((Lp . v) - (Lq . v)) by RLVECT_2:54 ;

A36: L . v >= 0 by Th62;

per cases
( v = p or v = q or ( v <> p & v <> q ) )
;

end;

suppose A37:
v = p
; :: thesis: Lpq . v >= 0

then
not v in Carrier Lq
by A15, A17, TARSKI:def 1;

then Lpq . v = (L . v) + (mm - 0) by A19, A35, A37;

hence Lpq . v >= 0 by A23, A36; :: thesis: verum

end;then Lpq . v = (L . v) + (mm - 0) by A19, A35, A37;

hence Lpq . v >= 0 by A23, A36; :: thesis: verum

.= 1 + 0 by A33, Th62 ;

then A42: L1pq is convex by A24, Th62;

then L1pq in ConvexComb V by CONVEX3:def 1;

then A43: Sum L1pq in conv A1 by A3, A42;

sum Lpq = (sum L) + (sum (Lp - Lq)) by Th34

.= 1 + 0 by A33, Th62 ;

then A44: Lpq is convex by A34, Th62;

then Lpq in ConvexComb V by CONVEX3:def 1;

then A45: Sum Lpq in conv A by A3, A44;

0. V = - (0. V) ;

then - (Sum (Lp - Lq)) <> 0. V by A32;

then Sum L1pq <> x by A5, A22, RLVECT_1:9;

then A46: Sum L1pq in (conv A) \ {x} by A43, ZFMISC_1:56;

Sum Lpq = (Sum L) + (Sum (Lp - Lq)) by RLVECT_3:1;

then Sum Lpq <> x by A5, A32, RLVECT_1:9;

then A47: Sum Lpq in (conv A) \ {x} by A45, ZFMISC_1:56;

((1 / 2) * (Sum Lpq)) + ((1 - (1 / 2)) * (Sum L1pq)) = ((1 / 2) * ((Sum L) + (Sum (Lp - Lq)))) + ((1 / 2) * ((Sum L) + (- (Sum (Lp - Lq))))) by A22, RLVECT_3:1

.= (((1 / 2) * (Sum L)) + ((1 / 2) * (Sum (Lp - Lq)))) + ((1 / 2) * ((Sum L) + (- (Sum (Lp - Lq))))) by RLVECT_1:def 5

.= (((1 / 2) * (Sum L)) + ((1 / 2) * (Sum (Lp - Lq)))) + (((1 / 2) * (Sum L)) + ((1 / 2) * (- (Sum (Lp - Lq))))) by RLVECT_1:def 5

.= ((1 / 2) * (Sum L)) + (((1 / 2) * (Sum (Lp - Lq))) + (((1 / 2) * (- (Sum (Lp - Lq)))) + ((1 / 2) * (Sum L)))) by RLVECT_1:def 3

.= ((1 / 2) * (Sum L)) + ((((1 / 2) * (Sum (Lp - Lq))) + ((1 / 2) * (- (Sum (Lp - Lq))))) + ((1 / 2) * (Sum L))) by RLVECT_1:def 3

.= ((1 / 2) * (Sum L)) + (((1 / 2) * ((Sum (Lp - Lq)) + (- (Sum (Lp - Lq))))) + ((1 / 2) * (Sum L))) by RLVECT_1:def 5

.= ((1 / 2) * (Sum L)) + (((1 / 2) * (0. V)) + ((1 / 2) * (Sum L))) by RLVECT_1:5

.= ((1 / 2) * (Sum L)) + ((0. V) + ((1 / 2) * (Sum L)))

.= ((1 / 2) * (Sum L)) + ((1 / 2) * (Sum L))

.= ((1 / 2) + (1 / 2)) * (Sum L) by RLVECT_1:def 6

.= Sum L by RLVECT_1:def 8 ;

then Sum L in (conv A) \ {x} by A2, A46, A47;

hence contradiction by A5, ZFMISC_1:56; :: thesis: verum