SIMPLEX1: Sperner's Lemma

:: Sperner's Lemma
:: by Karol P\c{a}k
::
:: Received February 9, 2010
:: Copyright (c) 2010-2011 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))

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

proof end;

end;

:: deftheorem defines @ SIMPLEX1:def 1 :

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

proof end;

end;

:: deftheorem defines @ SIMPLEX1:def 2 :

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 not S is dependent holds
Complex_of {(@ S)} is SubSimplicialComplex of K

proof end;

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
( not A is dependent & x in conv (@ A) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines |. SIMPLEX1:def 3 :

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 not A is dependent holds
conv (@ A) c= |.Kr.|

proof end;

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
( not A is dependent & 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

proof end;

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.| & ( for A being Subset of it st not A is dependent holds
ex B being Subset of Kr st
( not B is dependent & conv (@ A) c= conv (@ B) ) ) );
existence

proof end;

end;

:: deftheorem Def4 defines SubdivisionStr SIMPLEX1:def 4 :

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 SubdivisionStr of Kr;
coherence

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 SubdivisionStr of K;
existence

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 SubdivisionStr of Kv;
existence

proof end;

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

proof end;

end;

:: deftheorem Def5 defines BCS SIMPLEX1:def 5 :

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

proof end;

end;

:: deftheorem Def6 defines BCS SIMPLEX1:def 6 :

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;

Lm1: for n being Nat holds card n = n

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

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

proof end;

end;

begin

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 not A is dependent holds
@ A is affinely-independent ;

end;

:: deftheorem Def7 defines affinely-independent SIMPLEX1:def 7 :

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 not A is dependent & not B is dependent holds
(conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B));

end;

:: deftheorem Def8 defines simplex-join-closed SIMPLEX1:def 8 :

registration

let V be RealLinearSpace;
cluster empty-membered -> affinely-independent SimplicialComplexStr of the carrier of V;
coherence

proof end;

let F be affinely-independent Subset-Family of V;
cluster Complex_of F -> affinely-independent ;
coherence

proof end;

end;

registration

let RLS be non empty RLSStruct ;
cluster empty-membered -> simplex-join-closed SimplicialComplexStr of the carrier of RLS;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

let V be RealLinearSpace;
cluster non empty trivial affinely-independent Element of bool the carrier of V;
existence

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 SimplicialComplexStr of the carrier of V;
existence

proof end;

end;

registration

let V be RealLinearSpace;
let K be affinely-independent SimplicialComplexStr of V;
cluster -> affinely-independent SubSimplicialComplex of K;
coherence

proof end;

end;

registration

let V be RealLinearSpace;
let K be simplex-join-closed SimplicialComplexStr of V;
cluster -> simplex-join-closed SubSimplicialComplex of K;
coherence

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 not A is dependent & not B is dependent & 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 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 not As is dependent & not Bs is dependent & 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 not As is dependent & @ As is affinely-independent & not Bs is dependent 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

proof end;

let n be Nat;
cluster BCS (n,Ka) -> non void affinely-independent ;
coherence

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

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

proof end;

let n be Nat;
cluster BCS (n,K) -> non void simplex-join-closed ;
coherence

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;

Lm2: 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;

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

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;