greatestFib_lt

Mathlib.Data.Nat.Fib.Zeckendorf

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem greatestFib_lt : greatestFib m < n ↔ m < fib n :=
  lt_iff_lt_of_le_iff_le le_greatestFib

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

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

Разделы

Аффилиация

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