le_greatestFib

Mathlib.Data.Nat.Fib.Zeckendorf

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

← MathLib Explorer

English

For all m,n, m ≤ greatestFib(n) iff fib(m) ≤ n.

Русский

Для всех m,n: m ≤ greatestFib(n) эквивалально fib(m) ≤ n.

LaTeX

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

Lean4

@[simp]
theorem le_greatestFib : m ≤ greatestFib n ↔ fib m ≤ n :=
  ⟨fun h ↦ (fib_mono h).trans <| fib_greatestFib_le _, fun h ↦
    le_findGreatest (m.le_fib_add_one.trans <| add_le_add_right h _) h⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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