spineId_map_hornInclusion — Mathlib

English

The map of spineId along the horn inclusion equals the spineId of the standard simplex: map(horn.spineId i h0 hN) Λ[n+2,i].ι = stdSimplex.spineId(n+2).

Русский

Пусть отображение spineId по включению рога равно spineId стандартного симплекса: map(horn.spineId i h0 hN) Λ[n+2,i].ι = stdSimplex.spineId(n+2).

LaTeX

$$$\mathrm{Path.map}(\mathrm{horn.spineId}\, i\, h_0\, h_n)\, \Lambda[n+2,i].ι = \mathrm{stdSimplex.spineId}(n+2)$$$

Lean4

@[simp]
theorem spineId_map_hornInclusion {n : ℕ} (i : Fin (n + 3)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 2)) :
    Path.map (horn.spineId.{u} i h₀ hₙ) Λ[n + 2, i].ι = stdSimplex.spineId (n + 2) :=
  rfl

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