sum_nat_eq_add_sum_succ — Mathlib

English

For any f : ℕ → Cardinal, the sum over ℕ of f equals f(0) plus the sum over ℕ of f(n+1).

Русский

Для любого f : ℕ → Cardinal сумма по ℕ от f равна f(0) плюс сумма по ℕ от f(n+1).

LaTeX

$$$ \sum_{n \in \mathbb{N}} f(n) = f(0) + \sum_{n \in \mathbb{N}} f(n+1) $$$

Lean4

theorem sum_nat_eq_add_sum_succ (f : ℕ → Cardinal.{u}) : Cardinal.sum f = f 0 + Cardinal.sum fun i => f (i + 1) :=
  by
  refine (Equiv.sigmaNatSucc fun i => Quotient.out (f i)).cardinal_eq.trans ?_
  simp only [mk_sum, mk_out, lift_id, mk_sigma]

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