count_succ' — Mathlib

English

For a natural number n, count p (n+1) equals count of p shifted by 1 over n plus indicator of p 0.

Русский

Для натурального n: count p (n+1) = count(p(·+1), n) + 1_{p(0)}.

LaTeX

$$$$\operatorname{count}(p, n+1) = \operatorname{count}(\lambda k. p(k+1), n) + \begin{cases}1, & p(0) \\ 0, & \neg p(0)\end{cases}.$$$$

Lean4

theorem count_succ' (n : ℕ) : count p (n + 1) = count (fun k ↦ p (k + 1)) n + if p 0 then 1 else 0 := by
  rw [count_add', count_one]

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