antitoneOn_of_add_one_le — Mathlib

English

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

Русский

Если s удовлетворяет OrdConnected и для всех a не являющегося максимумом, f(a+1) ≤ f(a), то fantiоно на s.

LaTeX

$$$s.\mathrm{OrdConnected} \Rightarrow (\forall a\,(\neg \mathrm{IsMax}(a) \to a+1 \in s \to f(a+1) \le f(a))) \Rightarrow \mathrm{AntitoneOn}(f,s)$$$

Lean4

theorem antitoneOn_of_add_one_le (hs : s.OrdConnected) :
    (∀ a, ¬IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) ≤ f a) → AntitoneOn f s := by
  simpa [Order.succ_eq_add_one] using antitoneOn_of_succ_le hs (f := f)

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