d_succ — Mathlib

English

For n, d_{n+1} = whiskerLeft (functor R G (n+1)) (const R G) − whiskerRight (d_n) (I R G).

Русский

Для любого n: d_{n+1} = whiskerLeft(F_{n+1}, const) − whiskerRight(d_n, I).

LaTeX

$$$d_{n+1} = \\mathrm{whiskerLeft}(\\mathrm{functor}\\;R\\;G\\;(n+1))(\\mathrm{const}\\;R\\;G) - \\mathrm{whiskerRight}(d\\;n, I\\;R\\;G)$$$

Lean4

theorem d_succ (n : ℕ) :
    d R G (n + 1) = whiskerLeft (functor R G (n + 1)) (const R G) - (by exact whiskerRight (d R G n) (I R G)) :=
  rfl

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