limitRecOn_succ — Mathlib

English

Limit recursion at successor: limitRecOn (succ o) ... = H2 o (limitRecOn o ...).

Русский

Рекурсия по пределу на суктора: ...

LaTeX

$$$\forall o\, H_1\ H_2\ H_3,\ limitRecOn(\mathrm{succ}\ o, H_1, H_2, H_3) = H_2\ o\ (\mathrm{limitRecOn}\ o\ H_1\ H_2\ H_3)$$$

Lean4

@[simp]
theorem limitRecOn_succ {motive} (o H₁ H₂ H₃) :
    @limitRecOn motive (succ o) H₁ H₂ H₃ = H₂ o (@limitRecOn motive o H₁ H₂ H₃) :=
  SuccOrder.limitRecOn_succ ..

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