monotoneOn_of_le_add_one — Mathlib

English

If s is OrdConnected and every step a → a+1 inside s does not decrease f, then f is monotone on s.

Русский

Пусть s непрерывно относительно порядка; если для всех a, не являющегося максимумом, a, a+1 ∈ s и f(a) ≤ f(a+1), то f монотонна на s.

LaTeX

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

Lean4

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

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