mkHom_f_succ_succ — Mathlib

English

The degree n+2 component of mkHom is determined by succ applied to the previous two components.

Русский

Компонента mkHom на степени n+2 задаётся через succ применённый к предыдущим двумя компонентам.

LaTeX

$$$\\mathrm{mkHom}\\;\\mathrm{f}_{n+2} = \\mathrm{succ}\\,n\\; (\\mathrm{f}_n,\\mathrm{f}_{n+1},\\mathrm{comm}_{n,n+1})$.$$

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 (n + 1)⟩).1 :=
  by dsimp [mkHom, mkHomAux]

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