s_comp_π_succ — Mathlib

English

Describes how s composes with δ_0 in the simplicial object.

Русский

Определяет композицию s с δ_0 в симплициальном объекте.

LaTeX

$$$ s \circ δ_0 = δ_0 \circ s $$$

Lean4

theorem s_comp_π_succ (n : ℕ) (i : Fin (n + 1)) :
    ExtraDegeneracy.s f S n ≫ WidePullback.π _ i.succ =
      @WidePullback.π _ _ _ f.right (fun _ : Fin (n + 1) => f.left) (fun _ => f.hom) _ i :=
  by
  simp [ExtraDegeneracy.s]
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11119): @[simp] removed as the linter complains the LHS is not in normal form

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