strictAntiOn_of_lt_sub_one — Mathlib

English

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

Русский

Если s OrdConnected и для всех a, не минимального, f(a) < f(a−1) на s, то f строго антимонотонна на s.

LaTeX

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

Lean4

theorem strictAntiOn_of_lt_sub_one (hs : s.OrdConnected) :
    (∀ a, ¬IsMin a → a ∈ s → a - 1 ∈ s → f a < f (a - 1)) → StrictAntiOn f s := by
  simpa [Order.pred_eq_sub_one] using strictAntiOn_of_lt_pred hs (f := f)

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