greatestFib_mono

Mathlib.Data.Nat.Fib.Zeckendorf

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

English

If m ≤ n then greatestFib(m) ≤ greatestFib(n).

Русский

Если m ≤ n, то greatestFib(m) ≤ greatestFib(n).

LaTeX

$$$$ m \le n \Rightarrow \operatorname{greatestFib}(m) \le \operatorname{greatestFib}(n). $$$$

Lean4

theorem greatestFib_mono : Monotone greatestFib := fun _a _b hab ↦
  findGreatest_mono (fun _k ↦ hab.trans') <| add_le_add_right hab _

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

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

Разделы

Аффилиация

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