fib_mono

Mathlib.Data.Nat.Fib.Basic

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

English

The Fibonacci function is monotone: if a ≤ b, then fib(a) ≤ fib(b).

Русский

Функция Фибоначчи монотонна: если a ≤ b, то fib(a) ≤ fib(b).

LaTeX

$$a \le b \Rightarrow fib(a) \le fib(b)$$

Lean4

@[mono]
theorem fib_mono : Monotone fib :=
  monotone_nat_of_le_succ fun _ => fib_le_fib_succ

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

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

Разделы

Аффилиация

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