BarycentricSupportPositive.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Positivity after support restriction and epimorphic simplex maps

theorem OAI.Thomason.Construction.HornBarycentric.supportCoordinates_nonzero line 16
Source documentation
All coordinates on the ordered support are nonzero.
```
theorem supportCoordinates_nonzero {n : ℕ} (x : StdSimplex ℝ (Fin (n+1)))
    (k : Fin (supportLen x+1)) : (supportCoordinates x).weights k ≠ 0 := by
…
```
Mentions: OAI.Thomason.Construction.HornBarycentric.supportLen, OAI.Thomason.Construction.HornBarycentric.supportCoordinates

theorem OAI.Thomason.Construction.HornBarycentric.map_nonzero line 27

Source documentation

A surjective vertex map preserves nonvanishing of all barycentric coordinates.

theorem map_nonzero {m n : ℕ} (f : Fin (m+1) → Fin (n+1))
    (hf : Function.Surjective f) (x : StdSimplex ℝ (Fin (m+1)))
    (hx : ∀ i, x.weights i ≠ 0) (j : Fin (n+1)) :
    (StdSimplex.map f x).weights j ≠ 0 := by
…