fib_succ_eq_succ_sum — Mathlib

English

For every n, fib(n+1) equals 1 plus the sum of fib(k) for k = 0,...,n-1.

Русский

Для каждого n верно: fib(n+1) равно 1 плюс сумма fib(k) для k от 0 до n-1.

LaTeX

$$$$ \operatorname{fib}(n+1) = 1 + \sum_{k=0}^{n-1} \operatorname{fib}(k). $$$$

Lean4

theorem fib_succ_eq_succ_sum (n : ℕ) : fib (n + 1) = (∑ k ∈ Finset.range n, fib k) + 1 := by
  induction n with
  | zero => simp
  | succ n ih =>
    calc
      fib (n + 2) = fib n + fib (n + 1) := fib_add_two
      _ = (fib n + ∑ k ∈ Finset.range n, fib k) + 1 := by rw [ih, add_assoc]
      _ = (∑ k ∈ Finset.range (n + 1), fib k) + 1 := by simp [Finset.range_add_one]

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