SubdivisionIncidence.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Incidence counts for the concrete iterated simplex

The missing-rank alternative for an actual flag transports the old boundary count, or gives two completions around a retained old top face. Iteration therefore gives one incident top cell on the original boundary and two in the interior.

theorem OAI.Tingley.incidentTop_zero_eq_singleton line 20
Source documentation
At depth zero the unique top cell is the full original vertex set.
```
theorem incidentTop_zero_eq_singleton (m : ℕ) (s : Finset (IterVertex m 0)) :
    incidentTop m 0 s = {Finset.univ} := by
…
```
Mentions: OAI.Tingley.IterVertex, OAI.Tingley.incidentTop
theorem OAI.Tingley.faceCarrier_zero line 35
Source documentation
The initial carrier of a face is that face itself.
```
theorem faceCarrier_zero (m : ℕ) (s : Finset (IterVertex m 0)) :
    faceCarrier m 0 s = s := by
…
```
Mentions: OAI.Tingley.IterVertex, OAI.Tingley.faceCarrier
theorem OAI.Tingley.incidentTop_card_eq_if_boundary line 43
Source documentation
Actual codimension-one incidence for every positive-dimensional iterated standard simplex. The boundary condition refers to the original coordinates.
```
theorem incidentTop_card_eq_if_boundary {m k : ℕ} (hm : 0 < m) :
    ∀ {s : Finset (IterVertex m k)}, s ∈ codimFaces m k →
      (incidentTop m k s).card =
        if (faceCarrier m k s).card = m then 1 else 2 := by
…
```
Mentions: OAI.Tingley.IterVertex, OAI.Tingley.codimFaces, OAI.Tingley.incidentTop, OAI.Tingley.faceCarrier