monotoneOn_of_sub_one_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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