mkHom_f_succ_succ — Mathlib

English

Second alternate expression for the degree progression of mkHom using the coherence data.

Русский

Второе альтернативное выражение для перехода степеней mkHom через данные когерентности.

LaTeX

$$$$ f(n+2) = \\text{... продолжение через когерентность } $$$$

Lean4

@[simp]
theorem mkHom_f_succ_succ (n : ℕ) :
    (mkHom P Q zero one one_zero_comm succ).f (n + 2) =
      (succ n
          ⟨(mkHom P Q zero one one_zero_comm succ).f n, (mkHom P Q zero one one_zero_comm succ).f (n + 1),
            (mkHom P Q zero one one_zero_comm succ).comm (n + 1) n⟩).1 :=
  by dsimp [mkHom, mkHomAux]

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