fib_le_fib_succ

Mathlib.Data.Nat.Fib.Basic

URI: https://scilib.ai/kg/mathlib#Nat.fib_le_fib_succ

English

For all n, fib(n) ≤ fib(n+1).

Русский

Для всех n выполняется fib(n) ≤ fib(n+1).

LaTeX

$$fib(n) \le fib(n+1)$$

Lean4

theorem fib_le_fib_succ {n : ℕ} : fib n ≤ fib (n + 1) := by cases n <;> simp [fib_add_two]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru