greatestFib_eq_zero

Mathlib.Data.Nat.Fib.Zeckendorf

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

← MathLib Explorer

English

For all n with n ≠ 1, greatestFib(fib(n)) = n.

Русский

Для всех n, при n ≠ 1, greatestFib(fib(n)) = n.

LaTeX

$$$$ \forall \{n\}, n \neq 1 \Rightarrow \operatorname{greatestFib}(\operatorname{fib}(n)) = n. $$$$

Lean4

@[simp]
theorem greatestFib_eq_zero : greatestFib n = 0 ↔ n = 0 :=
  ⟨fun h ↦ by simpa using findGreatest_eq_zero_iff.1 h zero_lt_one le_add_self, by rintro rfl; rfl⟩

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

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

Разделы

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

Аффилиация

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