SpernerFacet.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The local facet count in geometric Sperner's lemma

A simplex with m + 1 vertices has an odd number of facets labelled by all labels except the last precisely when the simplex is fully labelled. The proof below identifies the good facets explicitly: one in the fully labelled case, and two whenever a good facet exists but the simplex is not full.

def OAI.Tingley.spernerSmallLabels line 19
Source documentation
The labels on the distinguished boundary face.
```
def spernerSmallLabels (m : ℕ) : Finset (Fin (m + 1)) :=
…
```
theorem OAI.Tingley.mem_spernerSmallLabels line 22
theorem OAI.Tingley.card_spernerSmallLabels line 26
def OAI.Tingley.spernerGoodFacets line 33
Source documentation
The codimension-one subsets carrying every label except the last.
```
def spernerGoodFacets (m : ℕ) (label : V → Fin (m + 1)) (σ : Finset V) :
    Finset (Finset V) :=
…
```
theorem OAI.Tingley.mem_spernerGoodFacets line 38

theorem OAI.Tingley.spernerGoodFacet_injOn line 46

Source documentation

A good facet has one vertex of each of its labels.

theorem spernerGoodFacet_injOn {label : V → Fin (m + 1)}
    {σ τ : Finset V} (hτ : τ ∈ spernerGoodFacets m label σ) :
    Set.InjOn label (↑τ : Set V) := by
…

Mentions: OAI.Tingley.spernerGoodFacets

theorem OAI.Tingley.spernerGoodFacets_card_of_full line 54

Source documentation

A fully labelled simplex has exactly one distinguished good facet.

theorem spernerGoodFacets_card_of_full (label : V → Fin (m + 1))
    (σ : Finset V) (hσ : σ.card = m + 1)
    (hfull : σ.image label = Finset.univ) :
    (spernerGoodFacets m label σ).card = 1 := by
…

Mentions: OAI.Tingley.spernerGoodFacets

theorem OAI.Tingley.spernerGoodFacets_card_of_nonempty_not_full line 112
Source documentation
In a non-full simplex, one good facet determines exactly two good facets. The second is obtained by exchanging the extra vertex with its equal-label partner in the first facet.
```
theorem spernerGoodFacets_card_of_nonempty_not_full
    (label : V → Fin (m + 1)) (σ : Finset V) (hσ : σ.card = m + 1)
    (hfull : σ.image label ≠ Finset.univ)
    (hne : (spernerGoodFacets m label σ).Nonempty) :
    (spernerGoodFacets m label σ).card = 2 := by
…
```
Mentions: OAI.Tingley.spernerGoodFacets

theorem OAI.Tingley.spernerGoodFacets_card_mod_two line 201

Source documentation

The local mod-two incidence identity, valid also in dimension zero.

theorem spernerGoodFacets_card_mod_two (label : V → Fin (m + 1))
    (σ : Finset V) (hσ : σ.card = m + 1) :
    ((spernerGoodFacets m label σ).card : ZMod 2) =
      if σ.image label = Finset.univ then 1 else 0 := by
…

Mentions: OAI.Tingley.spernerGoodFacets