fib_add_two — Mathlib

English

Let fib be the Fibonacci sequence. For every natural number n, fib(n+2) = fib(n) + fib(n+1).

Русский

Пусть fib обозначает последовательность Фибоначчи. Для каждого натурального числа n выполняется fib(n+2) = fib(n) + fib(n+1).

LaTeX

$$$fib(n+2) = fib(n) + fib(n+1)$$$

Lean4

/-- Shows that `fib` indeed satisfies the Fibonacci recurrence `Fₙ₊₂ = Fₙ + Fₙ₊₁.` -/
theorem fib_add_two {n : ℕ} : fib (n + 2) = fib n + fib (n + 1) := by simp [fib, Function.iterate_succ_apply']

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