:: Sperner's Lemma :: by Karol P\c{a}k :: :: Received February 9, 2010 :: Copyright (c) 2010-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ARYTM_1, ARYTM_3, XBOOLE_0, CARD_1, CARD_2, CLASSES1, COHSP_1, COMPLEX1, CONVEX1, CONVEX2, CONVEX3, FINSEQ_1, FINSET_1, FUNCT_1, MATROID0, MCART_1, ORDERS_1, PARTFUN1, PRE_TOPC, QC_LANG1, RELAT_1, RLVECT_1, RLVECT_2, SEMI_AF1, SETFAM_1, SGRAPH1, SUBSET_1, TARSKI, TOPS_1, ZFMISC_1, RLAFFIN1, RLAFFIN2, SIMPLEX0, SIMPLEX1, REAL_1, FUNCOP_1, NAT_1, FUNCT_2, STRUCT_0, XXREAL_0, NUMBERS, ORDINAL1, CARD_3, GLIB_000, FINSEQ_4; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XXREAL_3, XXREAL_0, XCMPLX_0, XREAL_0, ORDERS_1, CARD_1, REAL_1, FINSET_1, WELLORD2, SETFAM_1, DOMAIN_1, RELAT_1, FUNCT_1, FUNCT_2, RELSET_1, FINSEQ_1, STRUCT_0, CLASSES1, RVSUM_1, RLVECT_1, RLVECT_2, CONVEX1, CONVEX2, CONVEX3, PRE_TOPC, RLAFFIN1, FUNCOP_1, PENCIL_1, MATROID0, XTUPLE_0, MCART_1, CARD_2, COHSP_1, SIMPLEX0, RLAFFIN2; constructors BINOP_2, CONVEX1, CONVEX3, REAL_1, RVSUM_1, RLAFFIN1, SIMPLEX0, TOPS_2, BORSUK_1, COHSP_1, CARD_2, RLAFFIN2, XTUPLE_0; registrations CARD_1, FINSET_1, FUNCT_1, NAT_1, RELAT_1, RLVECT_1, STRUCT_0, SUBSET_1, VALUED_0, XCMPLX_0, XREAL_0, XXREAL_0, XBOOLE_0, RLAFFIN1, SIMPLEX0, FUNCOP_1, INT_1, XXREAL_3, MATROID0, SETFAM_1, COHSP_1, RLAFFIN2, RELSET_1, RLVECT_2, ORDINAL1, XTUPLE_0, FINSEQ_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Preliminaries reserve x,y,X for set, r for Real, n,k for Nat; theorem :: SIMPLEX1:1 for R be Relation, C be 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; theorem :: SIMPLEX1:2 for Y be non empty finite set st card X = card Y+1 for f be Function of X,Y st f is onto ex y st y in Y & card(f"{y}) = 2 & for x st x in Y & x <> y holds card (f"{x})=1; 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; end; 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; end; theorem :: SIMPLEX1:3 for X be 1-sorted for K be subset-closed SimplicialComplexStr of X st K is total for S be finite Subset of K st S is simplex-like holds Complex_of {@S} is SubSimplicialComplex of K; begin :: The Area of an Abstract Simplicial Complex reserve RLS for non empty RLSStruct, Kr,K1r,K2r for SimplicialComplexStr of RLS, V for RealLinearSpace, Kv for non void SimplicialComplex of V; definition let RLS,Kr; func |.Kr.| -> Subset of RLS means :: SIMPLEX1:def 3 x in it iff ex A be Subset of Kr st A is simplex-like & x in conv @A; end; theorem :: SIMPLEX1:4 the topology of K1r c= the topology of K2r implies |.K1r.| c= |.K2r.|; theorem :: SIMPLEX1:5 for A be Subset of Kr st A is simplex-like holds conv @A c= |.Kr.|; theorem :: SIMPLEX1:6 for K be subset-closed SimplicialComplexStr of V holds x in |.K.| iff ex A be Subset of K st A is simplex-like & x in Int @A; theorem :: SIMPLEX1:7 |.Kr.| is empty iff Kr is empty-membered; theorem :: SIMPLEX1:8 for A be Subset of RLS holds |.Complex_of{A}.| = conv A; theorem :: SIMPLEX1:9 for A,B be Subset-Family of RLS holds |.Complex_of (A\/B).| = |.Complex_of A.| \/ |.Complex_of B.|; begin :: The Subdivision of a Simplicial Complex definition let RLS,Kr; mode SubdivisionStr of Kr -> SimplicialComplexStr of RLS means :: SIMPLEX1:def 4 |.Kr.| c= |.it.| & for A be Subset of it st A is simplex-like ex B be Subset of Kr st B is simplex-like & conv @A c= conv @B; end; theorem :: SIMPLEX1:10 for P be SubdivisionStr of Kr holds |.Kr.| = |.P.|; registration let RLS; let Kr be with_non-empty_element SimplicialComplexStr of RLS; cluster -> with_non-empty_element for SubdivisionStr of Kr; end; theorem :: SIMPLEX1:11 Kr is SubdivisionStr of Kr; theorem :: SIMPLEX1:12 Complex_of the topology of Kr is SubdivisionStr of Kr; theorem :: SIMPLEX1:13 for K be subset-closed SimplicialComplexStr of V for SF be Subset-Family of K st SF = Sub_of_Fin the topology of K holds Complex_of SF is SubdivisionStr of K; theorem :: SIMPLEX1:14 for P1 be SubdivisionStr of Kr for P2 be SubdivisionStr of P1 holds P2 is SubdivisionStr of Kr; registration let V; let K be SimplicialComplexStr of V; cluster finite-membered subset-closed for SubdivisionStr of K; end; definition let V; let K be SimplicialComplexStr of V; mode Subdivision of K is finite-membered subset-closed SubdivisionStr of K; end; theorem :: SIMPLEX1:15 for K be with_empty_element SimplicialComplex of V st |.K.| c= [#]K for B be Function of BOOL the carrier of V,the carrier of V st for S be Simplex of K st S is non empty holds B.S in conv @S holds subdivision(B,K) is SubdivisionStr of K; registration let V,Kv; cluster non void for Subdivision of Kv; end; begin :: The Barycentric Subdivision definition let V,Kv such that |.Kv.| c= [#]Kv; func BCS Kv -> non void Subdivision of Kv equals :: SIMPLEX1:def 5 subdivision(center_of_mass V,Kv); end; definition let n; let V,Kv such that |.Kv.| c= [#]Kv; func BCS(n,Kv) -> non void Subdivision of Kv equals :: SIMPLEX1:def 6 subdivision(n,center_of_mass V,Kv); end; theorem :: SIMPLEX1:16 |.Kv.| c= [#]Kv implies BCS(0,Kv) = Kv; theorem :: SIMPLEX1:17 |.Kv.| c= [#]Kv implies BCS(1,Kv) = BCS Kv; theorem :: SIMPLEX1:18 |.Kv.| c= [#]Kv implies [#]BCS(n,Kv) = [#]Kv; theorem :: SIMPLEX1:19 |.Kv.| c= [#]Kv implies |.BCS(n,Kv).| = |.Kv.|; theorem :: SIMPLEX1:20 |.Kv.| c= [#]Kv implies BCS(n+1,Kv) = BCS BCS(n,Kv); theorem :: SIMPLEX1:21 |.Kv.| c= [#]Kv & degree Kv <= 0 implies the TopStruct of Kv = BCS Kv; theorem :: SIMPLEX1:22 n > 0 & |.Kv.| c= [#]Kv & degree Kv <= 0 implies the TopStruct of Kv = BCS(n,Kv); theorem :: SIMPLEX1:23 for Sv be non void SubSimplicialComplex of Kv st |.Kv.| c= [#]Kv & |.Sv.| c= [#]Sv holds BCS(n,Sv) is SubSimplicialComplex of BCS(n,Kv); theorem :: SIMPLEX1:24 |.Kv.| c= [#]Kv implies Vertices Kv c= Vertices BCS(n,Kv); registration let n,V; let K be non void total SimplicialComplex of V; cluster BCS(n,K) -> total; end; registration let n,V; let K be non void finite-vertices total SimplicialComplex of V; cluster BCS(n,K) -> finite-vertices; end; begin :: Selected Properties of Simplicial Complexes definition let V; let K be SimplicialComplexStr of V; attr K is affinely-independent means :: SIMPLEX1:def 7 for A be Subset of K st A is simplex-like holds @A is affinely-independent; end; definition let RLS,Kr; attr Kr is simplex-join-closed means :: SIMPLEX1:def 8 for A,B be Subset of Kr st A is simplex-like & B is simplex-like holds conv @A /\ conv @B = conv @(A/\B); end; registration let V; cluster empty-membered -> affinely-independent for SimplicialComplexStr of V; let F be affinely-independent Subset-Family of V; cluster Complex_of F -> affinely-independent; end; registration let RLS; cluster empty-membered -> simplex-join-closed for SimplicialComplexStr of RLS; end; registration let V; let I be affinely-independent Subset of V; cluster Complex_of{I} -> simplex-join-closed; end; registration let V; cluster 1-element affinely-independent for Subset of V; end; registration let V; cluster with_non-empty_element finite-vertices affinely-independent simplex-join-closed total for SimplicialComplex of V; end; registration let V; let K be affinely-independent SimplicialComplexStr of V; cluster -> affinely-independent for SubSimplicialComplex of K; end; registration let V; let K be simplex-join-closed SimplicialComplexStr of V; cluster -> simplex-join-closed for SubSimplicialComplex of K; end; theorem :: SIMPLEX1:25 for K be subset-closed SimplicialComplexStr of V holds K is simplex-join-closed iff for A,B be Subset of K st A is simplex-like & B is simplex-like & Int @A meets Int @B holds A=B; reserve Ks for simplex-join-closed SimplicialComplex of V, As,Bs for Subset of Ks, Ka for non void affinely-independent SimplicialComplex of V, Kas for non void affinely-independent simplex-join-closed SimplicialComplex of V, K for non void affinely-independent simplex-join-closed total SimplicialComplex of V; registration let V,Ka; let S be Simplex of Ka; cluster @S -> affinely-independent; end; theorem :: SIMPLEX1:26 As is simplex-like & Bs is simplex-like & Int@As meets conv@Bs implies As c= Bs; theorem :: SIMPLEX1:27 As is simplex-like & @As is affinely-independent & Bs is simplex-like implies (Int@As c= conv @Bs iff As c= Bs); theorem :: SIMPLEX1:28 |.Ka.| c= [#]Ka implies BCS Ka is affinely-independent; registration let V; let Ka be non void affinely-independent total SimplicialComplex of V; cluster BCS Ka -> affinely-independent; let n; cluster BCS(n,Ka) -> affinely-independent; end; registration let V,Kas; cluster (center_of_mass V)|the topology of Kas -> one-to-one; end; theorem :: SIMPLEX1:29 |.Kas.| c= [#]Kas implies BCS Kas is simplex-join-closed; registration let V,K; cluster BCS K -> simplex-join-closed; let n; cluster BCS(n,K) -> simplex-join-closed; end; theorem :: SIMPLEX1:30 |.Kv.| c= [#]Kv & (for n st n <= degree Kv ex S be Simplex of Kv st card S = n+1 & @S is affinely-independent) implies degree Kv = degree BCS Kv; theorem :: SIMPLEX1:31 |.Ka.| c= [#]Ka implies degree Ka = degree BCS Ka; theorem :: SIMPLEX1:32 |.Ka.| c= [#]Ka implies degree Ka = degree BCS(n,Ka); theorem :: SIMPLEX1:33 for S be simplex-like Subset-Family of Kas st S is with_non-empty_elements holds card S = card ((center_of_mass V).:S); reserve Aff for finite affinely-independent Subset of V, Af,Bf for finite Subset of V, B for Subset of V, S,T for finite Subset-Family of V, Sf for c=-linear finite finite-membered Subset-Family of V, Sk,Tk for finite simplex-like Subset-Family of K, Ak for Simplex of K; theorem :: SIMPLEX1:34 for S1,S2 be 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; theorem :: SIMPLEX1:35 S is with_non-empty_elements & union S c= Aff & card S+n+1 <= card Aff implies ( Bf is Simplex of n+card S,BCS Complex_of{Aff} & (center_of_mass V).:S c=Bf iff ex T st T misses S & T\/S is c=-linear with_non-empty_elements & card T=n+1 & union T c= Aff & Bf = (center_of_mass V).:S\/(center_of_mass V).:T); theorem :: SIMPLEX1:36 Sf is with_non-empty_elements & union Sf c=Aff implies ((center_of_mass V).:Sf is Simplex of card union Sf-1,BCS Complex_of {Aff} iff for n st 0 < n & n <= card union Sf ex x st x in Sf & card x = n); theorem :: SIMPLEX1:37 for S st S is c=-linear & S is with_non-empty_elements & card S = card union S for Af,Bf st Af is non 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}; theorem :: SIMPLEX1:38 for Sf st Sf is with_non-empty_elements & card Sf = card union Sf for v be 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}}}; theorem :: SIMPLEX1:39 for Sf 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; theorem :: SIMPLEX1:40 Aff is Simplex of K implies (B is Simplex of BCS Complex_of{Aff} iff B is Simplex of BCS K & conv B c= conv Aff); theorem :: SIMPLEX1:41 Sk is with_non-empty_elements & card Sk+n <= degree K implies (Af is Simplex of n+card Sk,BCS K & (center_of_mass V).:Sk c=Af iff ex Tk st Tk misses Sk & Tk\/Sk is c=-linear with_non-empty_elements & card Tk=n+1 & Af = (center_of_mass V).:Sk\/(center_of_mass V).:Tk); theorem :: SIMPLEX1:42 Sk is c=-linear with_non-empty_elements & card Sk = card union Sk & union Sk c= Ak & card Ak = card Sk+1 implies {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}}; theorem :: SIMPLEX1:43 Sk is c=-linear with_non-empty_elements & card Sk+1 = card union Sk implies 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; theorem :: SIMPLEX1:44 for Af st K is Subdivision of Complex_of{Af} & card Af = n+1 & degree K = n & for S be Simplex of n-1,K,X 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 be Simplex of n-1,BCS K,X 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); theorem :: SIMPLEX1:45 for S be 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); begin :: The Main Theorem reserve v for Vertex of BCS(k,Complex_of{Aff}), F for Function of Vertices BCS(k,Complex_of{Aff}),Aff; theorem :: SIMPLEX1:46 for F st for v,B st B c= Aff & v in conv B holds F.v in B ex n st card {S where S is Simplex of card Aff-1,BCS(k,Complex_of{Aff}): F.:S = Aff} = 2*n+1; :: Sperner's Lemma theorem :: SIMPLEX1:47 for F st for v,B st B c= Aff & v in conv B holds F.v in B ex S be Simplex of card Aff-1,BCS(k,Complex_of{Aff}) st F.:S = Aff;