BarycentricPurity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Purity of the actual finite face-chain subdivision

A finite chain can be completed at any positive rank below a retained upper face. A chain of maximum cardinality among the extensions of a given face therefore has every rank up to the dimension of an old top face.

theorem OAI.Tingley.FiniteComplex.chain_exists_insert_rank line 25
Source documentation
Insert an old face of a prescribed positive rank, provided the flag already contains some old face of at least that rank. The inserted face is allowed to be already present.
```
theorem chain_exists_insert_rank {c : Finset (FaceVertex K)} (hc : K.chain c)
    {r : ℕ} (hr : 0 < r) (hupper : ∃ U ∈ c, r ≤ U.val.card) :
    ∃ a : FaceVertex K, a.val.card = r ∧ K.chain (insert a c) := by
…
```
Mentions: OAI.Tingley.FiniteComplex.FaceVertex
theorem OAI.Tingley.FiniteComplex.chain_exists_top_upper line 65
Source documentation
In a pure old complex, every flag has a common old top face above it.
```
theorem chain_exists_top_upper {m : ℕ} (hK : K.Pure m)
    {c : Finset (FaceVertex K)} (hc : K.chain c) :
    ∃ T : FaceVertex K, T.val.card = m + 1 ∧ ∀ b ∈ c, b.val ⊆ T.val := by
…
```
Mentions: OAI.Tingley.FiniteComplex.FaceVertex
theorem OAI.Tingley.FiniteComplex.sd_pure line 84
Source documentation
Every face of the subdivision extends to an actual top flag.
```
theorem sd_pure {m : ℕ} (hK : K.Pure m) : K.sd.Pure m := by
…
```
theorem OAI.Tingley.iter_pure line 124
Source documentation
Every face of every iterated subdivision of the simplex extends to a top-dimensional face. The dimension-zero case is included.
```
theorem iter_pure (m k : ℕ) : (iterData (Fin (m + 1)) k).complex.Pure m := by
…
```
Mentions: OAI.Tingley.iterData