strictMonoOn_of_lt_add_one — Mathlib

English

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

Русский

Пусть s OrdConnected и для всех a верно f(a) < f(a+1) на паре a, а также a+1 ∈ s; тогда f строго возрастает на s.

LaTeX

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

Lean4

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

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