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