spineEquiv — Mathlib

English

The spineEquiv forms an equivalence between spine objects and Path objects at every level, respecting the StrictSegal structure.

Русский

SpineEquiv образует эквивалентность между структурами spine и Path на каждом уровне, совместимая со StrictSegal.

LaTeX

$$spineEquiv n : X_{⟨n⟩} ≃ Path X n$$

Lean4

/-- The fields of `StrictSegal` define an equivalence between `X _⦋n⦌`
and `Path X n`. -/
def spineEquiv (n : ℕ) : X _⦋n⦌ ≃ Path X n where
  toFun := X.spine n
  invFun := sx.spineToSimplex
  left_inv := sx.spineToSimplex_spine_apply
  right_inv := sx.spine_spineToSimplex_apply

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