OAI/Analysis/SphereIsometry/Sperner.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Geometric Sperner parity for the concrete iterated subdivisions

The labels belong to the actual recursively constructed vertex carriers. The incidence theorem and the exact original-face restriction discharge the finite counting hypotheses. Induction on dimension proves an odd number of fully labelled top cells at every subdivision depth.

  1. theorem OAI.Tingley.iterated_sperner_odd line 20
  2. theorem OAI.Tingley.iterated_sperner_exists line 91

    Source documentation

    Each actual subdivision contains an actual fully labelled top cell.

    theorem iterated_sperner_exists (m k : ℕ)
    (label : IterVertex m k → Fin (m + 1))
    (hlabel : ∀ v, label v ∈ iterCarrier m k v) :
    ∃ σ, σ ∈ topCells m k ∧ σ.image label = Finset.univ := by
…

    Mentions: OAI.Tingley.IterVertex, OAI.Tingley.iterCarrier, OAI.Tingley.topCells