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


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

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 & card (f " {y}) = 2 & ( for x being set st x in Y & x <> y holds
card (f " {x}) = 1 ) )
proof end;

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
proof end;
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
proof end;
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
proof end;

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 & 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 & x in conv (@ A) ) )
proof end;
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 & x in conv (@ A) ) ) ) & ( for x being set holds
( x in b2 iff ex A being Subset of Kr st
( A is simplex-like & x in conv (@ A) ) ) ) holds
b1 = b2
proof end;
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 & 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.|
proof end;

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.| by Def3;

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 & x in Int (@ A) ) )
proof end;

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 )
proof end;

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

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).|
proof end;

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.| & ( for A being Subset of it st A is simplex-like holds
ex B being Subset of Kr st
( B is simplex-like & conv (@ A) c= conv (@ B) ) ) );
existence
ex b1 being SimplicialComplexStr of RLS st
( |.Kr.| c= |.b1.| & ( for A being Subset of b1 st A is simplex-like holds
ex B being Subset of Kr st
( B is simplex-like & conv (@ A) c= conv (@ B) ) ) )
proof end;
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.| & ( for A being Subset of b3 st A is simplex-like holds
ex B being Subset of Kr st
( B is simplex-like & 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.|
proof end;

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
proof end;
end;

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

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
proof end;

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
proof end;

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
proof end;

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 & b1 is subset-closed )
proof end;
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
proof end;

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
proof end;
end;

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
proof end;
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 A1: |.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
proof end;
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
proof end;

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
proof end;

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
proof end;

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))
proof end;

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

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

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 & |.Sv.| c= [#] Sv holds
BCS (n,Sv) is SubSimplicialComplex of BCS (n,Kv)
proof end;

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))
proof end;

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
proof end;
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
proof end;
end;

definition
let V be RealLinearSpace;
let K be SimplicialComplexStr of V;
attr K 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;
attr Kr is simplex-join-closed means :Def8: :: SIMPLEX1:def 8
for A, B being Subset of Kr st A is simplex-like & 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 & 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
proof end;
let F be affinely-independent Subset-Family of V;
cluster Complex_of F -> affinely-independent ;
coherence
Complex_of F is affinely-independent
proof end;
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
proof end;
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
proof end;
end;

registration
let V be RealLinearSpace;
cluster 1 -element affinely-independent for Element of bool the carrier of V;
existence
ex b1 being Subset of V st
( b1 is 1 -element & b1 is affinely-independent )
proof end;
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 & b1 is finite-vertices & b1 is affinely-independent & b1 is simplex-join-closed & b1 is total )
proof end;
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
proof end;
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
proof end;
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 & B is simplex-like & Int (@ A) meets Int (@ B) holds
A = B )
proof end;

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 & Bs is simplex-like & Int (@ As) meets conv (@ Bs) holds
As c= Bs
proof end;

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 & @ As is affinely-independent & Bs is simplex-like holds
( Int (@ As) c= conv (@ Bs) iff As c= Bs )
proof end;

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
proof end;

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
proof end;
let n be Nat;
cluster BCS (n,Ka) -> non void affinely-independent ;
coherence
BCS (n,Ka) is affinely-independent
proof end;
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
proof end;
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
proof end;

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
proof end;
let n be Nat;
cluster BCS (n,K) -> non void simplex-join-closed ;
coherence
BCS (n,K) is simplex-join-closed
proof end;
end;

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

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)
proof end;

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))
proof end;

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)
proof end;

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 & S1 is with_non-empty_elements & (center_of_mass V) .: S2 is Simplex of (BCS Kas) & (center_of_mass V) .: S1 c= (center_of_mass V) .: S2 holds
( S1 c= S2 & S2 is c=-linear )
proof end;

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 & union S c= Aff & ((card S) + n) + 1 <= card Aff holds
( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st
( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )
proof end;

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 & 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 & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) )
proof end;

Lm1: for V being RealLinearSpace
for S being finite finite-membered Subset-Family of V st S is c=-linear & S is with_non-empty_elements & card S = card (union S) holds
for A being non empty finite Subset of V st A misses union S & (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)})

proof end;

theorem Th37: :: SIMPLEX1:37
for V being RealLinearSpace
for S being finite Subset-Family of V st S is c=-linear & S is with_non-empty_elements & card S = card (union S) holds
for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & (union S) \/ Af is affinely-independent & (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})
proof end;

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 & card Sf = card (union Sf) holds
for v being Element of V st not v in union Sf & (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})}))}
proof end;

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 & (card Sf) + 1 = card (union Sf) & 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
proof end;

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) & conv B c= conv Aff ) )
proof end;

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 & (card Sk) + n <= degree K holds
( ( Af is Simplex of n + (card Sk), BCS K & (center_of_mass V) .: Sk c= Af ) iff ex Tk being finite simplex-like Subset-Family of K st
( Tk misses Sk & Tk \/ Sk is c=-linear & Tk \/ Sk is with_non-empty_elements & card Tk = n + 1 & Af = ((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: Tk) ) )
proof end;

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 & Sk is with_non-empty_elements & card Sk = card (union Sk) & union Sk c= Ak & card Ak = (card Sk) + 1 holds
{ S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ Ak) ) } = {(((center_of_mass V) .: Sk) \/ ((center_of_mass V) .: {Ak}))}
proof end;

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 & Sk is with_non-empty_elements & (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 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2
proof end;

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} & card Af = n + 1 & degree K = n & ( 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 ) & ( 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 ) & ( conv (@ S) misses Int Af implies card X = 1 ) )
proof end;

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 & 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 ) & ( conv (@ S) misses Int Aff implies card X = 1 ) )
proof end;

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 & 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
proof end;

:: 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 & 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
proof end;