strictMonoOn_of_sub_one_lt — Mathlib

English

If s is OrdConnected and for all a, f(a−1) < f(a) on s, then f is strictly 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) < f(a)) \Rightarrow \mathrm{StrictMonoOn}(f,s)$$$

Lean4

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

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