Scarf.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Scarf incidence argument used to prove the fixed point principle needed for the simultaneous normalization. In spirit cf. Ivanov "Beyond Sperner's lemma". Here we use labels as extra ghost vertices so facets can use ordinary Finset inclusion.

structure OAI.GeneralMahler.Scarf.Orders line 17
def OAI.GeneralMahler.Scarf.dom line 23
Source comment
dominance formulated without choosing minima
```
def dom (s : Finset T) : Prop :=
…
```
lemma OAI.GeneralMahler.Scarf.dom_subset line 27
lemma OAI.GeneralMahler.Scarf.min_nodes line 33
lemma OAI.GeneralMahler.Scarf.min_cover line 40
lemma OAI.GeneralMahler.Scarf.image_erase_eq' line 54

lemma OAI.GeneralMahler.Scarf.duplicate_pair line 67

Source comment

unique pair of repeated indices of a map onto one-less elements

lemma duplicate_pair {s:Finset A} (u : A→B)
    (h : s.card = (s.image u).card+1) :
    ∃ a ∈ s, ∃ b ∈ s, a≠b ∧ u a=u b ∧
      ∀ i ∈ s, ∀ j ∈ s, i≠j → u i=u j → (i=a ∧ j=b) ∨ (i=b ∧ j=a) := by
…

def OAI.GeneralMahler.Scarf.room line 86
def OAI.GeneralMahler.Scarf.door line 87
def OAI.GeneralMahler.Scarf.cand line 90
Source comment
candidate replacements for each repeated index
```
def cand (u : I → T) (i : I) := Finset.univ.filter fun x =>
…
```
lemma OAI.GeneralMahler.Scarf.mem_cand' line 94
lemma OAI.GeneralMahler.Scarf.extension_spec line 97