antitone_of_le_sub_one

Mathlib.Algebra.Order.SuccPred

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem antitone_of_le_sub_one : (∀ a, ¬IsMin a → f a ≤ f (a - 1)) → Antitone f := by
  simpa [Order.pred_eq_sub_one] using antitone_of_le_pred (f := f)

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

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

Разделы

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

Аффилиация

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