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
proof
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;
then reconsider YY = { B where B is Subset of V : ( B c= If & ex x being set st
( 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
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;
A11: U c= If
proof
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;
U <> If
proof
defpred S1[ 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 & S1[x,y] )
proof
let x be object ; :: thesis: ( x in If implies ex y being object st
( y in bool If & S1[x,y] ) )
assume x in If ; :: thesis: ex y being object st
( y in bool If & S1[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 & S1[x,B] )
thus ( B in bool If & S1[x,B] ) by A16, A18; :: thesis: verum
end;
consider p being Function of If,(bool If) such that
A19: for x being object st x in If holds
S1[x,p . x] from FUNCT_2:sch 1(A15);
 defpred S2[ 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 & S2[x,y] )
proof
let x be object ; :: thesis: ( x in If implies ex y being object st
( y in the carrier of V & S2[x,y] ) )
assume A22: x in If ; :: thesis: ex y being object st
( y in the carrier of V & S2[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 & S2[x,y] )
thus ( y in the carrier of V & S2[x,y] ) by A23; :: thesis: verum
end;
consider q being Function of If,V such that
A24: for x being object st x in If holds
S2[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
proof
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;
then A28: R c= conv U by A4;
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)
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;
A39: R c= Carrier L
proof
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;
A41: conv U c= conv If by A11, RLAFFIN1:3;
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
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;
A66: now :: thesis: for m being Nat st m in dom F holds
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;
consider n being object such that
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;
Carrier ((Sum L) |-- If) c= If by RLVECT_2:def 6;
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;
hence ( U c< If & conv A c= conv U ) by A4, A11; :: thesis: verum