ofIsStrictSegal — Mathlib

English

The previous vertex identity holds at lt-case when i.castSucc < j.

Русский

Предыдущее тождество вершин сохраняется в lt-кейсе, если i.castSucc < j.

LaTeX

$$$hij : i.castSucc < j \Rightarrow (X.spine m (X.map (tr (δ j)).op (sx.spineToSimplex (m+1) f))).vertex i = f.vertex i.castSucc$$$

Lean4

/-- Given `IsStrictSegal X`, a choice of inverse to `spine X n` for all `n : ℕ`
determines an inhabitant of `StrictSegal X`. -/
noncomputable def ofIsStrictSegal [IsStrictSegal X] : StrictSegal X
    where
  spineToSimplex {n} := Equiv.ofBijective (X.spine n) (IsStrictSegal.segal n) |>.invFun
  spine_spineToSimplex n := funext <| Equiv.ofBijective (X.spine n) _ |>.right_inv
  spineToSimplex_spine n := funext <| Equiv.ofBijective (X.spine n) _ |>.left_inv

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