spineId — Mathlib

English

Any inner horn contains the spine of the unique nondegenerate n-simplex in Δ[n].

Русский

Любой внутренний рог содержит хребет уникального недегenerate n-симплекса в Δ[n].

LaTeX

$$$\text{spineId}_{n}(i,h_0,h_n) \in \mathrm{Path}(\Lambda[n+2,i], n+2)$$$

Lean4

/-- Any inner horn contains the spine of the unique non-degenerate `n`-simplex
in `Δ[n]`. -/
@[simps! vertex_coe arrow_coe]
def spineId {n : ℕ} (i : Fin (n + 3)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 2)) :
    Path (Λ[n + 2, i] : SSet.{u}) (n + 2) :=
  Λ[n + 2, i].liftPath (stdSimplex.spineId (n + 2)) (by simp)
    (fun j ↦ by
      convert (horn.primitiveEdge.{u} h₀ hₙ j).2
      ext a
      fin_cases a <;> rfl)

Похожие утверждения