monotone_of_sub_one_le

Mathlib.Algebra.Order.SuccPred

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

← MathLib Explorer

English

If for all a, f(a−1) ≤ f(a), then f is monotone.

Русский

Если для всех a выполняется f(a−1) ≤ f(a), то f монотонна.

LaTeX

$$$(\forall a, f(a-1) \le f(a)) \Rightarrow \mathrm{Monotone}(f)$$$

Lean4

theorem monotone_of_sub_one_le : (∀ a, ¬IsMin a → f (a - 1) ≤ f a) → Monotone f := by
  simpa [Order.pred_eq_sub_one] using monotone_of_pred_le (f := f)

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

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

Разделы

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

Аффилиация

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