antitoneOn_of_le_sub_one — Mathlib

English

If s is OrdConnected and for all a, f(a) ≤ f(a−1) on s, then f is antitone on s.

Русский

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

LaTeX

$$$s.\mathrm{OrdConnected} \Rightarrow (\forall a, \mathrm{IsPredSub}(a) \to f(a) \le f(a-1)) \Rightarrow \mathrm{AntitoneOn}(f,s)$$$

Lean4

theorem antitoneOn_of_le_sub_one (hs : s.OrdConnected) :
    (∀ a, ¬IsMin a → a ∈ s → a - 1 ∈ s → f a ≤ f (a - 1)) → AntitoneOn f s := by
  simpa [Order.pred_eq_sub_one] using antitoneOn_of_le_pred hs (f := f)

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