strictAntiOn_of_add_one_lt — Mathlib

English

If s is OrdConnected and for all a not maximal, f(a+1) < f(a), then f is strictly anti-monotone on s.

Русский

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

LaTeX

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

Lean4

theorem strictAntiOn_of_add_one_lt (hs : s.OrdConnected) :
    (∀ a, ¬IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) < f a) → StrictAntiOn f s := by
  simpa [Order.succ_eq_add_one] using strictAntiOn_of_succ_lt hs (f := f)

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