count_add' — Mathlib

English

For natural numbers a,b, count p (a+b) equals count of p shifted by b over a plus count p b.

Русский

Для натуральных a,b: count p (a+b) = count( p(·+b) , a) + count p b.

LaTeX

$$$$\operatorname{count}(p, a+b) = \operatorname{count}(\lambda k. p(k+b), a) + \operatorname{count}(p, b).$$$$

Lean4

theorem count_add' (a b : ℕ) : count p (a + b) = count (fun k ↦ p (k + b)) a + count p b :=
  by
  rw [add_comm, count_add, add_comm]
  simp_rw [add_comm b]

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