monotone_of_le_add_one — Mathlib

English

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

Русский

Пусть s OrdConnected и для всех a, не минимального, f(a−1) ≤ f(a) на s; тогда 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 monotone_of_le_add_one : (∀ a, ¬IsMax a → f a ≤ f (a + 1)) → Monotone f := by
  simpa [Order.succ_eq_add_one] using monotone_of_le_succ (f := f)

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