:: Sperner's Lemma
:: by Karol P\c{a}k
::
:: Received February 9, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

theorem Th1: :: SIMPLEX1:1
for X being set
for R being Relation
for C being Cardinal st ( for x being set st x in X holds
card (Im (R,x)) = C ) holds
card R = (card (R | ((dom R) \ X))) +` (C *` (card X))
proofend;

theorem Th2: :: SIMPLEX1:2
for X being set
for Y being non empty finite set st card X = (card Y) + 1 holds
for f being Function of X,Y st f is onto holds
ex y being set st
( y in Y &amp; card (f " {y}) = 2 &amp; ( for x being set st x in Y &amp; x <> y holds
card (f " {x}) = 1 ) )
proofend;

definition
let X be 1-sorted ;
mode SimplicialComplexStr of X is SimplicialComplexStr of the carrier of X;
mode SimplicialComplex of X is SimplicialComplex of the carrier of X;
end;

definition
let X be 1-sorted ;
let K be SimplicialComplexStr of X;
let A be Subset of K;
func @ A ->  Subset of X equals :: SIMPLEX1:def 1
A;
coherence
 A is Subset of X
proofend;
end;

:: deftheorem  defines @ SIMPLEX1:def_1_:_
 for X being 1-sorted
for K being SimplicialComplexStr of X
for A being Subset of K holds @ A = A;

definition
let X be 1-sorted ;
let K be SimplicialComplexStr of X;
let A be Subset-Family of K;
func @ A ->  Subset-Family of X equals :: SIMPLEX1:def 2
A;
coherence
 A is Subset-Family of X
proofend;
end;

:: deftheorem  defines @ SIMPLEX1:def_2_:_
 for X being 1-sorted
for K being SimplicialComplexStr of X
for A being Subset-Family of K holds @ A = A;

theorem Th3: :: SIMPLEX1:3
for X being 1-sorted
for K being subset-closed SimplicialComplexStr of X st K is total holds
for S being finite Subset of K st S is simplex-like holds
Complex_of {(@ S)} is SubSimplicialComplex of K
proofend;

begin

definition
let RLS be non empty RLSStruct ;
let Kr be SimplicialComplexStr of RLS;
func|.Kr.| ->  Subset of RLS means :Def3: :: SIMPLEX1:def 3
 for x being set holds
( x in it iff ex A being Subset of Kr st
( A is simplex-like &amp; x in conv (@ A) ) );
existence
 ex b1 being Subset of RLS st
for x being set holds
( x in b1 iff ex A being Subset of Kr st
( A is simplex-like &amp; x in conv (@ A) ) )
proofend;
uniqueness
 for b1, b2 being Subset of RLS st ( for x being set holds
( x in b1 iff ex A being Subset of Kr st
( A is simplex-like &amp; x in conv (@ A) ) ) ) &amp; ( for x being set holds
( x in b2 iff ex A being Subset of Kr st
( A is simplex-like &amp; x in conv (@ A) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines |. SIMPLEX1:def_3_:_
 for RLS being non empty RLSStruct
for Kr being SimplicialComplexStr of RLS
for b3 being Subset of RLS holds
( b3 = |.Kr.| iff for x being set holds
( x in b3 iff ex A being Subset of Kr st
( A is simplex-like &amp; x in conv (@ A) ) ) );

theorem Th4: :: SIMPLEX1:4
for RLS being non empty RLSStruct
for K1r, K2r being SimplicialComplexStr of RLS st the topology of K1r c= the topology of K2r holds
|.K1r.| c= |.K2r.|
proofend;

theorem Th5: :: SIMPLEX1:5
for RLS being non empty RLSStruct
for Kr being SimplicialComplexStr of RLS
for A being Subset of Kr st A is simplex-like holds
conv (@ A) c= |.Kr.|
proofend;

theorem :: SIMPLEX1:6
for x being set
for V being RealLinearSpace
for K being subset-closed SimplicialComplexStr of V holds
( x in |.K.| iff ex A being Subset of K st
( A is simplex-like &amp; x in Int (@ A) ) )
proofend;

theorem Th7: :: SIMPLEX1:7
for RLS being non empty RLSStruct
for Kr being SimplicialComplexStr of RLS holds
( |.Kr.| is empty iff Kr is empty-membered )
proofend;

theorem Th8: :: SIMPLEX1:8
for RLS being non empty RLSStruct
for A being Subset of RLS holds |.(Complex_of {A}).| = conv A
proofend;

theorem :: SIMPLEX1:9
for RLS being non empty RLSStruct
for A, B being Subset-Family of RLS holds |.(Complex_of (A \/ B)).| = |.(Complex_of A).| \/ |.(Complex_of B).|
proofend;

begin

definition
let RLS be non empty RLSStruct ;
let Kr be SimplicialComplexStr of RLS;
mode SubdivisionStr of Kr ->  SimplicialComplexStr of RLS means :Def4: :: SIMPLEX1:def 4
( |.Kr.| c= |.it.| &amp; ( for A being Subset of it st A is simplex-like holds
ex B being Subset of Kr st
( B is simplex-like &amp; conv (@ A) c= conv (@ B) ) ) );
existence
 ex b1 being SimplicialComplexStr of RLS st
( |.Kr.| c= |.b1.| &amp; ( for A being Subset of b1 st A is simplex-like holds
ex B being Subset of Kr st
( B is simplex-like &amp; conv (@ A) c= conv (@ B) ) ) )
proofend;
end;

:: deftheorem Def4 defines SubdivisionStr SIMPLEX1:def_4_:_
 for RLS being non empty RLSStruct
for Kr, b3 being SimplicialComplexStr of RLS holds
( b3 is SubdivisionStr of Kr iff ( |.Kr.| c= |.b3.| &amp; ( for A being Subset of b3 st A is simplex-like holds
ex B being Subset of Kr st
( B is simplex-like &amp; conv (@ A) c= conv (@ B) ) ) ) );

theorem Th10: :: SIMPLEX1:10
for RLS being non empty RLSStruct
for Kr being SimplicialComplexStr of RLS
for P being SubdivisionStr of Kr holds |.Kr.| = |.P.|
proofend;

registration
let RLS be non empty RLSStruct ;
let Kr be with_non-empty_element SimplicialComplexStr of RLS;
cluster  ->  with_non-empty_element for SubdivisionStr of Kr;
coherence
 for b1 being SubdivisionStr of Kr holds b1 is with_non-empty_element
proofend;
end;

theorem Th11: :: SIMPLEX1:11
for RLS being non empty RLSStruct
for Kr being SimplicialComplexStr of RLS holds Kr is SubdivisionStr of Kr
proofend;

theorem Th12: :: SIMPLEX1:12
for RLS being non empty RLSStruct
for Kr being SimplicialComplexStr of RLS holds Complex_of the topology of Kr is SubdivisionStr of Kr
proofend;

theorem Th13: :: SIMPLEX1:13
for V being RealLinearSpace
for K being subset-closed SimplicialComplexStr of V
for SF being Subset-Family of K st SF = Sub_of_Fin the topology of K holds
Complex_of SF is SubdivisionStr of K
proofend;

theorem Th14: :: SIMPLEX1:14
for RLS being non empty RLSStruct
for Kr being SimplicialComplexStr of RLS
for P1 being SubdivisionStr of Kr
for P2 being SubdivisionStr of P1 holds P2 is SubdivisionStr of Kr
proofend;

registration
let V be RealLinearSpace;
let K be SimplicialComplexStr of V;
cluster subset-closed finite-membered for SubdivisionStr of K;
existence
 ex b1 being SubdivisionStr of K st
( b1 is finite-membered &amp; b1 is subset-closed )
proofend;
end;

definition
let V be RealLinearSpace;
let K be SimplicialComplexStr of V;
mode Subdivision of K is subset-closed finite-membered SubdivisionStr of K;
end;

theorem Th15: :: SIMPLEX1:15
for V being RealLinearSpace
for K being with_empty_element SimplicialComplex of V st |.K.| c= [#] K holds
for B being Function of (BOOL the carrier of V), the carrier of V st ( for S being Simplex of K st not S is empty holds
B . S in conv (@ S) ) holds
subdivision (B,K) is SubdivisionStr of K
proofend;

registration
let V be RealLinearSpace;
let Kv be non void SimplicialComplex of V;
cluster non void subset-closed finite-membered for SubdivisionStr of Kv;
existence
 not for b1 being Subdivision of Kv holds b1 is void
proofend;
end;

begin

definition
let V be RealLinearSpace;
let Kv be non void SimplicialComplex of V;
assume A1: |.Kv.| c= [#] Kv ;
func BCS Kv ->  non void Subdivision of Kv equals :Def5: :: SIMPLEX1:def 5
 subdivision ((center_of_mass V),Kv);
coherence
 subdivision ((center_of_mass V),Kv) is non void Subdivision of Kv
proofend;
end;

:: deftheorem Def5 defines BCS SIMPLEX1:def_5_:_
 for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
BCS Kv = subdivision ((center_of_mass V),Kv);

definition
let n be Nat;
let V be RealLinearSpace;
let Kv be non void SimplicialComplex of V;
assume B1: |.Kv.| c= [#] Kv ;
func BCS (n,Kv) ->  non void Subdivision of Kv equals :Def6: :: SIMPLEX1:def 6
 subdivision (n,(center_of_mass V),Kv);
coherence
 subdivision (n,(center_of_mass V),Kv) is non void Subdivision of Kv
proofend;
end;

:: deftheorem Def6 defines BCS SIMPLEX1:def_6_:_
 for n being Nat
for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
BCS (n,Kv) = subdivision (n,(center_of_mass V),Kv);

theorem Th16: :: SIMPLEX1:16
for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
BCS (0,Kv) = Kv
proofend;

theorem Th17: :: SIMPLEX1:17
for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
BCS (1,Kv) = BCS Kv
proofend;

theorem Th18: :: SIMPLEX1:18
for n being Nat
for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
[#] (BCS (n,Kv)) = [#] Kv
proofend;

theorem :: SIMPLEX1:19
for n being Nat
for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
|.(BCS (n,Kv)).| = |.Kv.| by Th10;

theorem Th20: :: SIMPLEX1:20
for n being Nat
for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
BCS ((n + 1),Kv) = BCS (BCS (n,Kv))
proofend;

theorem Th21: :: SIMPLEX1:21
for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv &amp; degree Kv <= 0 holds
TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv
proofend;

theorem Th22: :: SIMPLEX1:22
for n being Nat
for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st n > 0 &amp; |.Kv.| c= [#] Kv &amp; degree Kv <= 0 holds
TopStruct(# the carrier of Kv, the topology of Kv #) = BCS (n,Kv)
proofend;

theorem Th23: :: SIMPLEX1:23
for n being Nat
for V being RealLinearSpace
for Kv being non void SimplicialComplex of V
for Sv being non void SubSimplicialComplex of Kv st |.Kv.| c= [#] Kv &amp; |.Sv.| c= [#] Sv holds
BCS (n,Sv) is SubSimplicialComplex of BCS (n,Kv)
proofend;

Lm1:  for n being Nat holds card n = n
proofend;

theorem Th24: :: SIMPLEX1:24
for n being Nat
for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
Vertices Kv c= Vertices (BCS (n,Kv))
proofend;

registration
let n be Nat;
let V be RealLinearSpace;
let K be non void total SimplicialComplex of V;
cluster BCS (n,K) ->  non void total ;
coherence
 BCS (n,K) is total
proofend;
end;

registration
let n be Nat;
let V be RealLinearSpace;
let K be non void finite-vertices total SimplicialComplex of V;
cluster BCS (n,K) ->  non void finite-vertices ;
coherence
 BCS (n,K) is finite-vertices
proofend;
end;

begin

definition
let V be RealLinearSpace;
let K be SimplicialComplexStr of V;
attrK is affinely-independent  means :Def7: :: SIMPLEX1:def 7
 for A being Subset of K st A is simplex-like holds
@ A is affinely-independent ;
end;

:: deftheorem Def7 defines affinely-independent SIMPLEX1:def_7_:_
 for V being RealLinearSpace
for K being SimplicialComplexStr of V holds
( K is affinely-independent iff for A being Subset of K st A is simplex-like holds
@ A is affinely-independent );

definition
let RLS be non empty RLSStruct ;
let Kr be SimplicialComplexStr of RLS;
attrKr is simplex-join-closed  means :Def8: :: SIMPLEX1:def 8
 for A, B being Subset of Kr st A is simplex-like &amp; B is simplex-like holds
(conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B));
end;

:: deftheorem Def8 defines simplex-join-closed SIMPLEX1:def_8_:_
 for RLS being non empty RLSStruct
for Kr being SimplicialComplexStr of RLS holds
( Kr is simplex-join-closed iff for A, B being Subset of Kr st A is simplex-like &amp; B is simplex-like holds
(conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) );

registration
let V be RealLinearSpace;
cluster empty-membered  ->  affinely-independent for SimplicialComplexStr of the carrier of V;
coherence
 for b1 being SimplicialComplexStr of V st b1 is empty-membered holds
b1 is affinely-independent
proofend;
let F be affinely-independent Subset-Family of V;
cluster Complex_of F ->  affinely-independent ;
coherence
 Complex_of F is affinely-independent
proofend;
end;

registration
let RLS be non empty RLSStruct ;
cluster empty-membered  ->  simplex-join-closed for SimplicialComplexStr of the carrier of RLS;
coherence
 for b1 being SimplicialComplexStr of RLS st b1 is empty-membered holds
b1 is simplex-join-closed
proofend;
end;

registration
let V be RealLinearSpace;
let I be affinely-independent Subset of V;
cluster Complex_of {I} ->  simplex-join-closed ;
coherence
 Complex_of {I} is simplex-join-closed
proofend;
end;

registration
let V be RealLinearSpace;
cluster1 -element affinely-independent for Element of bool the carrier of V;
existence
 ex b1 being Subset of V st
( b1 is 1 -element &amp; b1 is affinely-independent )
proofend;
end;

registration
let V be RealLinearSpace;
cluster subset-closed finite-membered finite-vertices with_non-empty_element total affinely-independent simplex-join-closed for SimplicialComplexStr of the carrier of V;
existence
 ex b1 being SimplicialComplex of V st
( b1 is with_non-empty_element &amp; b1 is finite-vertices &amp; b1 is affinely-independent &amp; b1 is simplex-join-closed &amp; b1 is total )
proofend;
end;

registration
let V be RealLinearSpace;
let K be affinely-independent SimplicialComplexStr of V;
cluster  ->  affinely-independent for SubSimplicialComplex of K;
coherence
 for b1 being SubSimplicialComplex of K holds b1 is affinely-independent
proofend;
end;

registration
let V be RealLinearSpace;
let K be simplex-join-closed SimplicialComplexStr of V;
cluster  ->  simplex-join-closed for SubSimplicialComplex of K;
coherence
 for b1 being SubSimplicialComplex of K holds b1 is simplex-join-closed
proofend;
end;

theorem Th25: :: SIMPLEX1:25
for V being RealLinearSpace
for K being subset-closed SimplicialComplexStr of V holds
( K is simplex-join-closed iff for A, B being Subset of K st A is simplex-like &amp; B is simplex-like &amp; Int (@ A) meets Int (@ B) holds
A = B )
proofend;

registration
let V be RealLinearSpace;
let Ka be non void affinely-independent SimplicialComplex of V;
let S be Simplex of Ka;
cluster @ S ->  affinely-independent ;
coherence
 @ S is affinely-independent by Def7;
end;

theorem Th26: :: SIMPLEX1:26
for V being RealLinearSpace
for Ks being simplex-join-closed SimplicialComplex of V
for As, Bs being Subset of Ks st As is simplex-like &amp; Bs is simplex-like &amp; Int (@ As) meets conv (@ Bs) holds
As c= Bs
proofend;

theorem :: SIMPLEX1:27
for V being RealLinearSpace
for Ks being simplex-join-closed SimplicialComplex of V
for As, Bs being Subset of Ks st As is simplex-like &amp; @ As is affinely-independent &amp; Bs is simplex-like holds
( Int (@ As) c= conv (@ Bs) iff As c= Bs )
proofend;

theorem Th28: :: SIMPLEX1:28
for V being RealLinearSpace
for Ka being non void affinely-independent SimplicialComplex of V st |.Ka.| c= [#] Ka holds
BCS Ka is affinely-independent
proofend;

registration
let V be RealLinearSpace;
let Ka be non void total affinely-independent SimplicialComplex of V;
cluster BCS Ka ->  non void affinely-independent ;
coherence
 BCS Ka is affinely-independent
proofend;
let n be Nat;
cluster BCS (n,Ka) ->  non void affinely-independent ;
coherence
 BCS (n,Ka) is affinely-independent
proofend;
end;

registration
let V be RealLinearSpace;
let Kas be non void affinely-independent simplex-join-closed SimplicialComplex of V;
cluster(center_of_mass V) | the topology of Kas ->  one-to-one ;
coherence
 (center_of_mass V) | the topology of Kas is one-to-one
proofend;
end;

theorem Th29: :: SIMPLEX1:29
for V being RealLinearSpace
for Kas being non void affinely-independent simplex-join-closed SimplicialComplex of V st |.Kas.| c= [#] Kas holds
BCS Kas is simplex-join-closed
proofend;

registration
let V be RealLinearSpace;
let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V;
cluster BCS K ->  non void simplex-join-closed ;
coherence
 BCS K is simplex-join-closed
proofend;
let n be Nat;
cluster BCS (n,K) ->  non void simplex-join-closed ;
coherence
 BCS (n,K) is simplex-join-closed
proofend;
end;

theorem Th30: :: SIMPLEX1:30
for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv &amp; ( for n being Nat st n <= degree Kv holds
ex S being Simplex of Kv st
( card S = n + 1 &amp; @ S is affinely-independent ) ) holds
degree Kv = degree (BCS Kv)
proofend;

theorem Th31: :: SIMPLEX1:31
for V being RealLinearSpace
for Ka being non void affinely-independent SimplicialComplex of V st |.Ka.| c= [#] Ka holds
degree Ka = degree (BCS Ka)
proofend;

theorem Th32: :: SIMPLEX1:32
for n being Nat
for V being RealLinearSpace
for Ka being non void affinely-independent SimplicialComplex of V st |.Ka.| c= [#] Ka holds
degree Ka = degree (BCS (n,Ka))
proofend;

theorem Th33: :: SIMPLEX1:33
for V being RealLinearSpace
for Kas being non void affinely-independent simplex-join-closed SimplicialComplex of V
for S being simplex-like Subset-Family of Kas st S is with_non-empty_elements holds
card S = card ((center_of_mass V) .: S)
proofend;

theorem Th34: :: SIMPLEX1:34
for V being RealLinearSpace
for Kas being non void affinely-independent simplex-join-closed SimplicialComplex of V
for S1, S2 being simplex-like Subset-Family of Kas st |.Kas.| c= [#] Kas &amp; S1 is with_non-empty_elements &amp; (center_of_mass V) .: S2 is Simplex of (BCS Kas) &amp; (center_of_mass V) .: S1 c= (center_of_mass V) .: S2 holds
( S1 c= S2 &amp; S2 is c=-linear )
proofend;

theorem Th35: :: SIMPLEX1:35
for n being Nat
for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for Bf being finite Subset of V
for S being finite Subset-Family of V st S is with_non-empty_elements &amp; union S c= Aff &amp; ((card S) + n) + 1 <= card Aff holds
( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) &amp; (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st
( T misses S &amp; T \/ S is c=-linear &amp; T \/ S is with_non-empty_elements &amp; card T = n + 1 &amp; union T c= Aff &amp; Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )
proofend;

theorem Th36: :: SIMPLEX1:36
for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements &amp; union Sf c= Aff holds
( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n &amp; n <= card (union Sf) holds
ex x being set st
( x in Sf &amp; card x = n ) )
proofend;

Lm2:  for V being RealLinearSpace
for S being finite finite-membered Subset-Family of V st S is c=-linear &amp; S is with_non-empty_elements &amp; card S = card (union S) holds
for A being non empty finite Subset of V st A misses union S &amp; (union S) \/ A is affinely-independent holds
((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)})
proofend;

theorem Th37: :: SIMPLEX1:37
for V being RealLinearSpace
for S being finite Subset-Family of V st S is c=-linear &amp; S is with_non-empty_elements &amp; card S = card (union S) holds
for Af, Bf being finite Subset of V st not Af is empty &amp; Af misses union S &amp; (union S) \/ Af is affinely-independent &amp; (union S) \/ Af c= Bf holds
((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ Af)}) is Simplex of card S, BCS (Complex_of {Bf})
proofend;

theorem Th38: :: SIMPLEX1:38
for V being RealLinearSpace
for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements &amp; card Sf = card (union Sf) holds
for v being Element of V st not v in union Sf &amp; (union Sf) \/ {v} is affinely-independent holds
{  S1 where S1 is Simplex of card Sf, BCS (Complex_of {((union Sf) \/ {v})}) : (center_of_mass V) .: Sf c= S1  }  = {(((center_of_mass V) .: Sf) \/ ((center_of_mass V) .: {((union Sf) \/ {v})}))}
proofend;

theorem Th39: :: SIMPLEX1:39
for V being RealLinearSpace
for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements &amp; (card Sf) + 1 = card (union Sf) &amp; union Sf is affinely-independent holds
card  {  S1 where S1 is Simplex of card Sf, BCS (Complex_of {(union Sf)}) : (center_of_mass V) .: Sf c= S1  }  = 2
proofend;

theorem Th40: :: SIMPLEX1:40
for V being RealLinearSpace
for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V
for Aff being finite affinely-independent Subset of V
for B being Subset of V st Aff is Simplex of K holds
( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) &amp; conv B c= conv Aff ) )
proofend;

theorem Th41: :: SIMPLEX1:41
for n being Nat
for V being RealLinearSpace
for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V
for Af being finite Subset of V
for Sk being finite simplex-like Subset-Family of K st Sk is with_non-empty_elements &amp; (card Sk) + n <= degree K holds
( ( Af is Simplex of n + (card Sk), BCS K &amp; (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st
( Tk misses Sk &amp; Tk \/ Sk is c=-linear &amp; Tk \/ Sk is with_non-empty_elements &amp; card Tk = n + 1 &amp; Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )
proofend;

theorem Th42: :: SIMPLEX1:42
for V being RealLinearSpace
for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V
for Sk being finite simplex-like Subset-Family of K
for Ak being Simplex of K st Sk is c=-linear &amp; Sk is with_non-empty_elements &amp; card Sk = card (union Sk) &amp; union Sk c= Ak &amp; card Ak = (card Sk) + 1 holds
{  S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 &amp; conv (@ S1) c= conv (@ Ak) )  }  = {(((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: {Ak}))}
proofend;

theorem Th43: :: SIMPLEX1:43
for V being RealLinearSpace
for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V
for Sk being finite simplex-like Subset-Family of K st Sk is c=-linear &amp; Sk is with_non-empty_elements &amp; (card Sk) + 1 = card (union Sk) holds
card  {  S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 &amp; conv (@ S1) c= conv (@ (union Sk)) )  }  = 2
proofend;

theorem Th44: :: SIMPLEX1:44
for n being Nat
for V being RealLinearSpace
for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V
for Af being finite Subset of V st K is Subdivision of Complex_of {Af} &amp; card Af = n + 1 &amp; degree K = n &amp; ( for S being Simplex of n - 1,K
for X being set st X =  {  S1 where S1 is Simplex of n,K : S c= S1  }  holds
( ( conv (@ S) meets Int Af implies card X = 2 ) &amp; ( conv (@ S) misses Int Af implies card X = 1 ) ) ) holds
for S being Simplex of n - 1, BCS K
for X being set st X =  {  S1 where S1 is Simplex of n, BCS K : S c= S1  }  holds
( ( conv (@ S) meets Int Af implies card X = 2 ) &amp; ( conv (@ S) misses Int Af implies card X = 1 ) )
proofend;

theorem Th45: :: SIMPLEX1:45
for X being set
for n, k being Nat
for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for S being Simplex of n - 1, BCS (k,(Complex_of {Aff})) st card Aff = n + 1 &amp; X =  {  S1 where S1 is Simplex of n, BCS (k,(Complex_of {Aff})) : S c= S1  }  holds
( ( conv (@ S) meets Int Aff implies card X = 2 ) &amp; ( conv (@ S) misses Int Aff implies card X = 1 ) )
proofend;

begin

theorem Th46: :: SIMPLEX1:46
for k being Nat
for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff &amp; v in conv B holds
F . v in B ) holds
ex n being Nat st card  {  S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff  }  = (2 * n) + 1
proofend;

:: Sperner's Lemma
theorem :: SIMPLEX1:47
for k being Nat
for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff &amp; v in conv B holds
F . v in B ) holds
ex S being Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) st F .: S = Aff
proofend;