fib_add_two_strictMono

Mathlib.Data.Nat.Fib.Basic

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

← MathLib Explorer

English

The function n ↦ fib(n+2) is strictly increasing.

Русский

Функция n ↦ fib(n+2) строго возрастает.

LaTeX

$$fib(n+2) \text{ is strictly increasing in } n$$

Lean4

/-- `fib (n + 2)` is strictly monotone. -/
theorem fib_add_two_strictMono : StrictMono fun n => fib (n + 2) :=
  by
  refine strictMono_nat_of_lt_succ fun n => ?_
  rw [add_right_comm]
  exact fib_lt_fib_succ (self_le_add_left _ _)

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

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

Разделы

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

Аффилиация

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