fib_succ_eq_sum_choose — Mathlib

English

For every natural number n, fib(n+1) equals the sum over all pairs (i,j) with i+j=n of binomial(i,j).

Русский

Для каждого натурального n fib(n+1) равняется сумме биномиальных коэффициентов по всем парам (i,j) such that i+j=n.

LaTeX

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

Lean4

theorem fib_succ_eq_sum_choose : ∀ n : ℕ, fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, choose p.1 p.2 :=
  twoStepInduction rfl rfl fun n h1 h2 =>
    by
    rw [fib_add_two, h1, h2, Finset.Nat.antidiagonal_succ_succ', Finset.Nat.antidiagonal_succ']
    simp [choose_succ_succ, Finset.sum_add_distrib, add_left_comm]

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