let V be RealLinearSpace; :: thesis: for A being Subset of V

for If being finite affinely-independent Subset of V st conv A c= conv If & not If is empty & conv A misses Int If holds

ex B being Subset of V st

( B c< If & conv A c= conv B )

let A be Subset of V; :: thesis: for If being finite affinely-independent Subset of V st conv A c= conv If & not If is empty & conv A misses Int If holds

ex B being Subset of V st

( B c< If & conv A c= conv B )

let If be finite affinely-independent Subset of V; :: thesis: ( conv A c= conv If & not If is empty & conv A misses Int If implies ex B being Subset of V st

( B c< If & conv A c= conv B ) )

assume that

A1: conv A c= conv If and

A2: not If is empty and

A3: conv A misses Int If ; :: thesis: ex B being Subset of V st

( B c< If & conv A c= conv B )

reconsider If = If as non empty finite affinely-independent Subset of V by A2;

set YY = { B where B is Subset of V : ( B c= If & ex x being set st

( x in conv A & x in Int B ) ) } ;

{ B where B is Subset of V : ( B c= If & ex x being set st

( x in conv A & x in Int B ) ) } c= bool the carrier of V

( x in conv A & x in Int B ) ) } as Subset-Family of V ;

take U = union YY; :: thesis: ( U c< If & conv A c= conv U )

A4: conv A c= conv U

for If being finite affinely-independent Subset of V st conv A c= conv If & not If is empty & conv A misses Int If holds

ex B being Subset of V st

( B c< If & conv A c= conv B )

let A be Subset of V; :: thesis: for If being finite affinely-independent Subset of V st conv A c= conv If & not If is empty & conv A misses Int If holds

ex B being Subset of V st

( B c< If & conv A c= conv B )

let If be finite affinely-independent Subset of V; :: thesis: ( conv A c= conv If & not If is empty & conv A misses Int If implies ex B being Subset of V st

( B c< If & conv A c= conv B ) )

assume that

A1: conv A c= conv If and

A2: not If is empty and

A3: conv A misses Int If ; :: thesis: ex B being Subset of V st

( B c< If & conv A c= conv B )

reconsider If = If as non empty finite affinely-independent Subset of V by A2;

set YY = { B where B is Subset of V : ( B c= If & ex x being set st

( x in conv A & x in Int B ) ) } ;

{ B where B is Subset of V : ( B c= If & ex x being set st

( x in conv A & x in Int B ) ) } c= bool the carrier of V

proof

then reconsider YY = { B where B is Subset of V : ( B c= If & ex x being set st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { B where B is Subset of V : ( B c= If & ex x being set st

( x in conv A & x in Int B ) ) } or x in bool the carrier of V )

assume x in { B where B is Subset of V : ( B c= If & ex x being set st

( x in conv A & x in Int B ) ) } ; :: thesis: x in bool the carrier of V

then ex B being Subset of V st

( B = x & B c= If & ex y being set st

( y in conv A & y in Int B ) ) ;

hence x in bool the carrier of V ; :: thesis: verum

end;( x in conv A & x in Int B ) ) } or x in bool the carrier of V )

assume x in { B where B is Subset of V : ( B c= If & ex x being set st

( x in conv A & x in Int B ) ) } ; :: thesis: x in bool the carrier of V

then ex B being Subset of V st

( B = x & B c= If & ex y being set st

( y in conv A & y in Int B ) ) ;

hence x in bool the carrier of V ; :: thesis: verum

( x in conv A & x in Int B ) ) } as Subset-Family of V ;

take U = union YY; :: thesis: ( U c< If & conv A c= conv U )

A4: conv A c= conv U

proof

A11:
U c= If
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in conv A or v in conv U )

assume A5: v in conv A ; :: thesis: v in conv U

then v in conv If by A1;

then v in union { (Int B) where B is Subset of V : B c= If } by Th8;

then consider IB being set such that

A6: v in IB and

A7: IB in { (Int B) where B is Subset of V : B c= If } by TARSKI:def 4;

consider B being Subset of V such that

A8: IB = Int B and

A9: B c= If by A7;

Int B c= conv B by Lm2;

then A10: v in conv B by A6, A8;

B in YY by A5, A6, A8, A9;

then conv B c= conv U by RLAFFIN1:3, ZFMISC_1:74;

hence v in conv U by A10; :: thesis: verum

end;assume A5: v in conv A ; :: thesis: v in conv U

then v in conv If by A1;

then v in union { (Int B) where B is Subset of V : B c= If } by Th8;

then consider IB being set such that

A6: v in IB and

A7: IB in { (Int B) where B is Subset of V : B c= If } by TARSKI:def 4;

consider B being Subset of V such that

A8: IB = Int B and

A9: B c= If by A7;

Int B c= conv B by Lm2;

then A10: v in conv B by A6, A8;

B in YY by A5, A6, A8, A9;

then conv B c= conv U by RLAFFIN1:3, ZFMISC_1:74;

hence v in conv U by A10; :: thesis: verum

proof

U <> If
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in U or x in If )

assume x in U ; :: thesis: x in If

then consider b being set such that

A12: x in b and

A13: b in YY by TARSKI:def 4;

ex B being Subset of V st

( b = B & B c= If & ex y being set st

( y in conv A & y in Int B ) ) by A13;

hence x in If by A12; :: thesis: verum

end;assume x in U ; :: thesis: x in If

then consider b being set such that

A12: x in b and

A13: b in YY by TARSKI:def 4;

ex B being Subset of V st

( b = B & B c= If & ex y being set st

( y in conv A & y in Int B ) ) by A13;

hence x in If by A12; :: thesis: verum

proof

hence
( U c< If & conv A c= conv U )
by A4, A11; :: thesis: verum
defpred S_{1}[ object , object ] means for B being Subset of V st B = $2 holds

( $1 in B & ex x being set st

( x in conv A & x in Int B ) );

assume A14: U = If ; :: thesis: contradiction

A15: for x being object st x in If holds

ex y being object st

( y in bool If & S_{1}[x,y] )

A19: for x being object st x in If holds

S_{1}[x,p . x]
from FUNCT_2:sch 1(A15);

defpred S_{2}[ object , object ] means for B being Subset of V st B = p . $1 holds

( $2 in conv A & $2 in Int B );

A20: dom p = If by FUNCT_2:def 1;

A21: for x being object st x in If holds

ex y being object st

( y in the carrier of V & S_{2}[x,y] )

A24: for x being object st x in If holds

S_{2}[x,q . x]
from FUNCT_2:sch 1(A21);

reconsider R = rng q as non empty finite Subset of V ;

A25: R c= conv A

A29: conv R c= conv A by A25, CONVEX1:30;

A30: dom q = If by FUNCT_2:def 1;

A31: (1 / (card R)) * (card R) = (card R) / (card R) by XCMPLX_1:99

.= 1 by XCMPLX_1:60 ;

consider L being Linear_Combination of R such that

A32: Sum L = (1 / (card R)) * (Sum R) and

A33: sum L = (1 / (card R)) * (card R) and

A34: L = (ZeroLC V) +* (R --> (1 / (card R))) by Th15;

set SL = Sum L;

set SLIf = (Sum L) |-- If;

Sum L = (center_of_mass V) . R by A32, Def2;

then A35: Sum L in conv R by Th16;

A36: dom (R --> (1 / (card R))) = R ;

then A42: R c= conv If by A28;

then A43: conv R c= conv If by CONVEX1:30;

then A44: Sum L in conv If by A35;

A45: R c= conv If by A28, A41;

Carrier L c= R by RLVECT_2:def 6;

then A46: R = Carrier L by A39;

A47: If c= Carrier ((Sum L) |-- If)

then ( Carrier ((Sum L) |-- If) = If & (Sum L) |-- If is convex ) by A47, A35, A43, RLAFFIN1:71;

then ( conv If c= Affin If & Sum ((Sum L) |-- If) in Int If ) by Th12, RLAFFIN1:65;

then Sum L in Int If by A44, RLAFFIN1:def 7;

hence contradiction by A3, A29, A35, XBOOLE_0:3; :: thesis: verum

end;( $1 in B & ex x being set st

( x in conv A & x in Int B ) );

assume A14: U = If ; :: thesis: contradiction

A15: for x being object st x in If holds

ex y being object st

( y in bool If & S

proof

consider p being Function of If,(bool If) such that
let x be object ; :: thesis: ( x in If implies ex y being object st

( y in bool If & S_{1}[x,y] ) )

assume x in If ; :: thesis: ex y being object st

( y in bool If & S_{1}[x,y] )

then consider b being set such that

A16: x in b and

A17: b in YY by A14, TARSKI:def 4;

consider B being Subset of V such that

A18: ( b = B & B c= If & ex y being set st

( y in conv A & y in Int B ) ) by A17;

take B ; :: thesis: ( B in bool If & S_{1}[x,B] )

thus ( B in bool If & S_{1}[x,B] )
by A16, A18; :: thesis: verum

end;( y in bool If & S

assume x in If ; :: thesis: ex y being object st

( y in bool If & S

then consider b being set such that

A16: x in b and

A17: b in YY by A14, TARSKI:def 4;

consider B being Subset of V such that

A18: ( b = B & B c= If & ex y being set st

( y in conv A & y in Int B ) ) by A17;

take B ; :: thesis: ( B in bool If & S

thus ( B in bool If & S

A19: for x being object st x in If holds

S

defpred S

( $2 in conv A & $2 in Int B );

A20: dom p = If by FUNCT_2:def 1;

A21: for x being object st x in If holds

ex y being object st

( y in the carrier of V & S

proof

consider q being Function of If,V such that
let x be object ; :: thesis: ( x in If implies ex y being object st

( y in the carrier of V & S_{2}[x,y] ) )

assume A22: x in If ; :: thesis: ex y being object st

( y in the carrier of V & S_{2}[x,y] )

then p . x in rng p by A20, FUNCT_1:def 3;

then reconsider px = p . x as Subset of V by XBOOLE_1:1;

consider y being set such that

A23: ( y in conv A & y in Int px ) by A19, A22;

take y ; :: thesis: ( y in the carrier of V & S_{2}[x,y] )

thus ( y in the carrier of V & S_{2}[x,y] )
by A23; :: thesis: verum

end;( y in the carrier of V & S

assume A22: x in If ; :: thesis: ex y being object st

( y in the carrier of V & S

then p . x in rng p by A20, FUNCT_1:def 3;

then reconsider px = p . x as Subset of V by XBOOLE_1:1;

consider y being set such that

A23: ( y in conv A & y in Int px ) by A19, A22;

take y ; :: thesis: ( y in the carrier of V & S

thus ( y in the carrier of V & S

A24: for x being object st x in If holds

S

reconsider R = rng q as non empty finite Subset of V ;

A25: R c= conv A

proof

then A28:
R c= conv U
by A4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in R or y in conv A )

assume y in R ; :: thesis: y in conv A

then consider x being object such that

A26: x in dom q and

A27: y = q . x by FUNCT_1:def 3;

p . x in rng p by A20, A26, FUNCT_1:def 3;

then reconsider px = p . x as Subset of V by XBOOLE_1:1;

px = p . x ;

hence y in conv A by A24, A26, A27; :: thesis: verum

end;assume y in R ; :: thesis: y in conv A

then consider x being object such that

A26: x in dom q and

A27: y = q . x by FUNCT_1:def 3;

p . x in rng p by A20, A26, FUNCT_1:def 3;

then reconsider px = p . x as Subset of V by XBOOLE_1:1;

px = p . x ;

hence y in conv A by A24, A26, A27; :: thesis: verum

A29: conv R c= conv A by A25, CONVEX1:30;

A30: dom q = If by FUNCT_2:def 1;

A31: (1 / (card R)) * (card R) = (card R) / (card R) by XCMPLX_1:99

.= 1 by XCMPLX_1:60 ;

consider L being Linear_Combination of R such that

A32: Sum L = (1 / (card R)) * (Sum R) and

A33: sum L = (1 / (card R)) * (card R) and

A34: L = (ZeroLC V) +* (R --> (1 / (card R))) by Th15;

set SL = Sum L;

set SLIf = (Sum L) |-- If;

Sum L = (center_of_mass V) . R by A32, Def2;

then A35: Sum L in conv R by Th16;

A36: dom (R --> (1 / (card R))) = R ;

A37: now :: thesis: for x being set st x in R holds

L . x = 1 / (card R)

A39:
R c= Carrier L
L . x = 1 / (card R)

let x be set ; :: thesis: ( x in R implies L . x = 1 / (card R) )

assume A38: x in R ; :: thesis: L . x = 1 / (card R)

hence L . x = (R --> (1 / (card R))) . x by A34, A36, FUNCT_4:13

.= 1 / (card R) by A38, FUNCOP_1:7 ;

:: thesis: verum

end;assume A38: x in R ; :: thesis: L . x = 1 / (card R)

hence L . x = (R --> (1 / (card R))) . x by A34, A36, FUNCT_4:13

.= 1 / (card R) by A38, FUNCOP_1:7 ;

:: thesis: verum

proof

A41:
conv U c= conv If
by A11, RLAFFIN1:3;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R or x in Carrier L )

assume A40: x in R ; :: thesis: x in Carrier L

then L . x <> 0 by A37;

hence x in Carrier L by A40; :: thesis: verum

end;assume A40: x in R ; :: thesis: x in Carrier L

then L . x <> 0 by A37;

hence x in Carrier L by A40; :: thesis: verum

then A42: R c= conv If by A28;

then A43: conv R c= conv If by CONVEX1:30;

then A44: Sum L in conv If by A35;

A45: R c= conv If by A28, A41;

Carrier L c= R by RLVECT_2:def 6;

then A46: R = Carrier L by A39;

A47: If c= Carrier ((Sum L) |-- If)

proof

Carrier ((Sum L) |-- If) c= If
by RLVECT_2:def 6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in If or x in Carrier ((Sum L) |-- If) )

assume A48: x in If ; :: thesis: x in Carrier ((Sum L) |-- If)

then consider F being FinSequence of REAL , G being FinSequence of V such that

A49: ((Sum L) |-- If) . x = Sum F and

A50: len G = len F and

G is one-to-one and

A51: rng G = Carrier L and

A52: for n being Nat st n in dom F holds

F . n = (L . (G . n)) * (((G . n) |-- If) . x) by A31, A33, A42, Th3;

A53: p . x in rng p by A20, A48, FUNCT_1:def 3;

then reconsider px = p . x as Subset of V by XBOOLE_1:1;

A54: Int px c= conv px by Lm2;

A55: q . x in Int px by A24, A48;

then A56: q . x in conv px by A54;

A57: x in px by A19, A48;

A58: conv px c= Affin px by RLAFFIN1:65;

A59: px is affinely-independent by A53, RLAFFIN1:43;

then Sum ((q . x) |-- px) = q . x by A56, A58, RLAFFIN1:def 7;

then A60: Carrier ((q . x) |-- px) = px by A54, A55, A59, Th11, RLAFFIN1:71;

(q . x) |-- px = (q . x) |-- If by A53, A56, A58, RLAFFIN1:77;

then A61: ((q . x) |-- If) . x <> 0 by A57, A60, RLVECT_2:19;

conv px c= conv If by A53, RLAFFIN1:3;

then A62: ((q . x) |-- If) . x >= 0 by A48, A56, RLAFFIN1:71;

A63: q . x in R by A30, A48, FUNCT_1:def 3;

then A64: L . (q . x) = 1 / (card R) by A37;

A65: dom G = dom F by A50, FINSEQ_3:29;

A69: n in dom G and

A70: G . n = q . x by A39, A51, A63, FUNCT_1:def 3;

F . n = (L . (q . x)) * (((q . x) |-- If) . x) by A52, A65, A69, A70;

then ((Sum L) |-- If) . x > 0 by A49, A61, A62, A64, A65, A66, A69, RVSUM_1:85;

hence x in Carrier ((Sum L) |-- If) by A48; :: thesis: verum

end;assume A48: x in If ; :: thesis: x in Carrier ((Sum L) |-- If)

then consider F being FinSequence of REAL , G being FinSequence of V such that

A49: ((Sum L) |-- If) . x = Sum F and

A50: len G = len F and

G is one-to-one and

A51: rng G = Carrier L and

A52: for n being Nat st n in dom F holds

F . n = (L . (G . n)) * (((G . n) |-- If) . x) by A31, A33, A42, Th3;

A53: p . x in rng p by A20, A48, FUNCT_1:def 3;

then reconsider px = p . x as Subset of V by XBOOLE_1:1;

A54: Int px c= conv px by Lm2;

A55: q . x in Int px by A24, A48;

then A56: q . x in conv px by A54;

A57: x in px by A19, A48;

A58: conv px c= Affin px by RLAFFIN1:65;

A59: px is affinely-independent by A53, RLAFFIN1:43;

then Sum ((q . x) |-- px) = q . x by A56, A58, RLAFFIN1:def 7;

then A60: Carrier ((q . x) |-- px) = px by A54, A55, A59, Th11, RLAFFIN1:71;

(q . x) |-- px = (q . x) |-- If by A53, A56, A58, RLAFFIN1:77;

then A61: ((q . x) |-- If) . x <> 0 by A57, A60, RLVECT_2:19;

conv px c= conv If by A53, RLAFFIN1:3;

then A62: ((q . x) |-- If) . x >= 0 by A48, A56, RLAFFIN1:71;

A63: q . x in R by A30, A48, FUNCT_1:def 3;

then A64: L . (q . x) = 1 / (card R) by A37;

A65: dom G = dom F by A50, FINSEQ_3:29;

A66: now :: thesis: for m being Nat st m in dom F holds

0 <= F . m

consider n being object such that 0 <= F . m

let m be Nat; :: thesis: ( m in dom F implies 0 <= F . m )

assume A67: m in dom F ; :: thesis: 0 <= F . m

then G . m in R by A46, A51, A65, FUNCT_1:def 3;

then A68: ( L . (G . m) > 0 & ((G . m) |-- If) . x >= 0 ) by A37, A45, A48, RLAFFIN1:71;

F . m = (L . (G . m)) * (((G . m) |-- If) . x) by A52, A67;

hence 0 <= F . m by A68; :: thesis: verum

end;assume A67: m in dom F ; :: thesis: 0 <= F . m

then G . m in R by A46, A51, A65, FUNCT_1:def 3;

then A68: ( L . (G . m) > 0 & ((G . m) |-- If) . x >= 0 ) by A37, A45, A48, RLAFFIN1:71;

F . m = (L . (G . m)) * (((G . m) |-- If) . x) by A52, A67;

hence 0 <= F . m by A68; :: thesis: verum

A69: n in dom G and

A70: G . n = q . x by A39, A51, A63, FUNCT_1:def 3;

F . n = (L . (q . x)) * (((q . x) |-- If) . x) by A52, A65, A69, A70;

then ((Sum L) |-- If) . x > 0 by A49, A61, A62, A64, A65, A66, A69, RVSUM_1:85;

hence x in Carrier ((Sum L) |-- If) by A48; :: thesis: verum

then ( Carrier ((Sum L) |-- If) = If & (Sum L) |-- If is convex ) by A47, A35, A43, RLAFFIN1:71;

then ( conv If c= Affin If & Sum ((Sum L) |-- If) in Int If ) by Th12, RLAFFIN1:65;

then Sum L in Int If by A44, RLAFFIN1:def 7;

hence contradiction by A3, A29, A35, XBOOLE_0:3; :: thesis: verum