let n be Nat; for A being non empty affinely-independent Subset of (TOP-REAL n)
for E being Enumeration of A
for F being FinSequence of bool the carrier of ((TOP-REAL n) | (conv A)) st len F = card A & rng F is closed & ( for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S) ) holds
not meet (rng F) is empty
set TRn = TOP-REAL n;
let A be non empty affinely-independent Subset of (TOP-REAL n); for E being Enumeration of A
for F being FinSequence of bool the carrier of ((TOP-REAL n) | (conv A)) st len F = card A & rng F is closed & ( for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S) ) holds
not meet (rng F) is empty
set cA = conv A;
let E be Enumeration of A; for F being FinSequence of bool the carrier of ((TOP-REAL n) | (conv A)) st len F = card A & rng F is closed & ( for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S) ) holds
not meet (rng F) is empty
let F be FinSequence of bool the carrier of ((TOP-REAL n) | (conv A)); ( len F = card A & rng F is closed & ( for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S) ) implies not meet (rng F) is empty )
assume that
A1:
len F = card A
and
A2:
rng F is closed
and
A3:
for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S)
; not meet (rng F) is empty
A4:
F <> {}
by A1;
A5:
rng E = A
by RLAFFIN3:def 1;
then
len E = card A
by FINSEQ_4:62;
then A6:
dom E = dom F
by A1, FINSEQ_3:29;
set En = Euclid n;
set Comp = Complex_of {A};
defpred S1[ object , object ] means ( $1 in F . ((E ") . $2) & ( for B being Subset of (TOP-REAL n) st B c= A & $1 in conv B holds
$2 in B ) );
A7:
TopSpaceMetr (Euclid n) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #)
by EUCLID:def 8;
then reconsider CA = conv A as non empty Subset of (TopSpaceMetr (Euclid n)) ;
reconsider ca = conv A as non empty Subset of (Euclid n) by A7;
A8:
(TopSpaceMetr (Euclid n)) | CA = TopSpaceMetr ((Euclid n) | ca)
by HAUSDORF:16;
then reconsider CrF = COMPLEMENT (rng F) as Subset-Family of (TopSpaceMetr ((Euclid n) | ca)) by A7, PRE_TOPC:36;
CA is compact
by A7, COMPTS_1:23;
then A9:
TopSpaceMetr ((Euclid n) | ca) is compact
by A8, COMPTS_1:3;
A10:
(TopSpaceMetr (Euclid n)) | CA = (TOP-REAL n) | (conv A)
by A7, PRE_TOPC:36;
assume
meet (rng F) is empty
; contradiction
then [#] ((TOP-REAL n) | (conv A)) =
(meet (rng F)) `
.=
union CrF
by A4, TOPS_2:7
;
then A11:
CrF is Cover of (TopSpaceMetr ((Euclid n) | ca))
by A8, A10, SETFAM_1:45;
set L = the Lebesgue_number of CrF;
A12:
|.(Complex_of {A}).| c= [#] (Complex_of {A})
;
then consider k being Nat such that
A13:
diameter (BCS (k,(Complex_of {A}))) < the Lebesgue_number of CrF
by Th18;
set Bcs = BCS (k,(Complex_of {A}));
A14:
|.(BCS (k,(Complex_of {A}))).| = |.(Complex_of {A}).|
by A12, SIMPLEX1:19;
A15:
the topology of (Complex_of {A}) = bool A
by SIMPLEX0:4;
A16:
for x being object st x in Vertices (BCS (k,(Complex_of {A}))) holds
ex y being object st
( y in A & S1[x,y] )
proof
let x be
object ;
( x in Vertices (BCS (k,(Complex_of {A}))) implies ex y being object st
( y in A & S1[x,y] ) )
assume A17:
x in Vertices (BCS (k,(Complex_of {A})))
;
ex y being object st
( y in A & S1[x,y] )
then reconsider v =
x as
Element of
(BCS (k,(Complex_of {A}))) ;
v is
vertex-like
by A17, SIMPLEX0:def 4;
then consider S being
Subset of
(BCS (k,(Complex_of {A}))) such that A18:
S is
simplex-like
and A19:
v in S
;
@ S c= conv (@ S)
by RLAFFIN1:2;
then A20:
v in conv (@ S)
by A19;
conv (@ S) c= |.(Complex_of {A}).|
by A14, A18, SIMPLEX1:5;
then consider W being
Subset of
(Complex_of {A}) such that A21:
W is
simplex-like
and A22:
v in Int (@ W)
by A20, SIMPLEX1:6;
A23:
v in conv (@ W)
by A22, RLAFFIN2:def 1;
A24:
W in the
topology of
(Complex_of {A})
by A21, PRE_TOPC:def 2;
then
(
E " W c= dom E &
E .: (E " W) = W )
by A5, A15, FUNCT_1:77, RELAT_1:132;
then
conv (@ W) c= union (F .: (E " W))
by A3, A6;
then consider Y being
set such that A25:
v in Y
and A26:
Y in F .: (E " W)
by A23, TARSKI:def 4;
consider i being
object such that
i in dom F
and A27:
i in E " W
and A28:
F . i = Y
by A26, FUNCT_1:def 6;
take y =
E . i;
( y in A & S1[x,y] )
A29:
y in W
by A27, FUNCT_1:def 7;
i in dom E
by A27, FUNCT_1:def 7;
hence
(
y in A &
x in F . ((E ") . y) )
by A15, A24, A25, A28, A29, FUNCT_1:34;
for B being Subset of (TOP-REAL n) st B c= A & x in conv B holds
y in B
let B be
Subset of
(TOP-REAL n);
( B c= A & x in conv B implies y in B )
assume that A30:
B c= A
and A31:
x in conv B
;
y in B
reconsider b =
B as
Simplex of
(Complex_of {A}) by A15, A30, PRE_TOPC:def 2;
conv (@ b) meets Int (@ W)
by A22, A31, XBOOLE_0:3;
then
W c= b
by A21, SIMPLEX1:26;
hence
y in B
by A29;
verum
end;
consider G being Function of (Vertices (BCS (k,(Complex_of {A})))),A such that
A32:
for x being object st x in Vertices (BCS (k,(Complex_of {A}))) holds
S1[x,G . x]
from FUNCT_2:sch 1(A16);
A33:
|.(Complex_of {A}).| = conv A
by SIMPLEX1:8;
then
BCS (k,(Complex_of {A})) is with_non-empty_element
by A14, SIMPLEX1:7;
then
for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of (TOP-REAL n) st B c= A & v in conv B holds
G . v in B
by A32;
then consider S being Simplex of (card A) - 1, BCS (k,(Complex_of {A})) such that
A34:
G .: S = A
by SIMPLEX1:47;
A35:
[#] (BCS (k,(Complex_of {A}))) = [#] (Complex_of {A})
by A12, SIMPLEX1:18;
then reconsider SS = S as Subset of (Euclid n) by A7;
not S is empty
by A34;
then consider s being object such that
A36:
s in S
by XBOOLE_0:def 1;
A37:
conv (@ S) c= conv A
by A14, A33, SIMPLEX1:5;
reconsider s = s as Point of (Euclid n) by A7, A35, A36;
A38:
S c= conv (@ S)
by RLAFFIN1:2;
then
s in conv (@ S)
by A36;
then reconsider ss = s as Point of ((Euclid n) | ca) by A37, TOPMETR:def 2;
A39:
SS is bounded
;
CrF is open
by A2, A8, A10, TOPS_2:9;
then consider CRF being Subset of (TopSpaceMetr ((Euclid n) | ca)) such that
A40:
CRF in CrF
and
A41:
Ball (ss, the Lebesgue_number of CrF) c= CRF
by A9, A11, Def1;
CRF ` in rng F
by A8, A10, A40, SETFAM_1:def 7;
then consider i being object such that
A42:
i in dom F
and
A43:
F . i = CRF `
by FUNCT_1:def 3;
E . i in A
by A5, A6, A42, FUNCT_1:def 3;
then consider w being object such that
A44:
w in dom G
and
A45:
w in S
and
A46:
G . w = E . i
by A34, FUNCT_1:def 6;
A47:
w in conv (@ S)
by A38, A45;
A48:
conv (@ S) c= conv A
by A14, A33, SIMPLEX1:5;
then A49:
( [#] ((Euclid n) | ca) = ca & w in conv A )
by A47, TOPMETR:def 2;
reconsider SS = S as bounded Subset of (Euclid n) by A39;
diameter SS <= diameter (BCS (k,(Complex_of {A})))
by Def4;
then A50:
diameter SS < the Lebesgue_number of CrF
by A13, XXREAL_0:2;
w in F . ((E ") . (G . w))
by A32, A44;
then A51:
w in F . i
by A6, A42, A46, FUNCT_1:34;
reconsider w = w as Point of (Euclid n) by A49;
reconsider ww = w as Point of ((Euclid n) | ca) by A47, A48, TOPMETR:def 2;
conv (@ S) c= cl_Ball (s,(diameter SS))
by A36, A38, Th13;
then
( dist (s,w) = dist (ss,ww) & dist (s,w) <= diameter SS )
by A47, METRIC_1:12, TOPMETR:def 1;
then
dist (ss,ww) < the Lebesgue_number of CrF
by A50, XXREAL_0:2;
then
ww in Ball (ss, the Lebesgue_number of CrF)
by METRIC_1:11;
hence
contradiction
by A41, A43, A51, XBOOLE_0:def 5; verum