strictMono_of_lt_add_one

Mathlib.Algebra.Order.SuccPred

URI: https://scilib.ai/kg/mathlib#strictMono_of_lt_add_one

← MathLib Explorer

English

If for all a, f(a) < f(a+1), then f is strictly monotone.

Русский

Если для всех a выполняется f(a) < f(a+1), то f строго монотонна.

LaTeX

$$$(\forall a, f(a) < f(a+1)) \Rightarrow \mathrm{StrictMono}(f)$$$

Lean4

theorem strictMono_of_lt_add_one : (∀ a, ¬IsMax a → f a < f (a + 1)) → StrictMono f := by
  simpa [Order.succ_eq_add_one] using strictMono_of_lt_succ (f := f)

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

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

Разделы

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

Аффилиация

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