spine_spineToSimplex_apply — Mathlib

English

If sx is a StrictSegal structure, spine m → simplex map is inverse to spineToSimplex.

Русский

Если X строгий сегал, стрелка spine к simplex обратно взаимна.

LaTeX

$$spine_spineToSimplex_apply {m} {h} (f : Path X m) : X.spine m h (sx.spineToSimplex m h f) = f$$

Lean4

@[simp]
theorem spine_spineToSimplex_apply (m : ℕ) (h : m ≤ n + 1) (f : Path X m) : X.spine m h (sx.spineToSimplex m h f) = f :=
  congr_fun (sx.spine_spineToSimplex m h) f

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