fib_strictMonoOn

Mathlib.Data.Nat.Fib.Basic

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

English

Fib is strictly increasing on the domain n ≥ 2.

Русский

Fibономи Фибоначчи строго возрастает на области n ≥ 2.

LaTeX

$$For all x

Lean4

theorem fib_strictMonoOn : StrictMonoOn fib (Set.Ici 2)
  | _m + 2, _, _n + 2, _, hmn => fib_add_two_strictMono <| lt_of_add_lt_add_right hmn

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

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

Разделы

Аффилиация

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