antitone_of_add_one_le

Mathlib.Algebra.Order.SuccPred

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

← MathLib Explorer

English

If for all a, f(a+1) ≤ f(a), then f is antitone.

Русский

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

LaTeX

$$$(\forall a, f(a+1) \le f(a)) \Rightarrow \mathrm{Antitone}(f)$$$

Lean4

theorem antitone_of_add_one_le : (∀ a, ¬IsMax a → f (a + 1) ≤ f a) → Antitone f := by
  simpa [Order.succ_eq_add_one] using antitone_of_succ_le (f := f)

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

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

Разделы

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

Аффилиация

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