strictMono_of_lt_succ — Mathlib

English

If for all a not maximal we have f(a) < f(succ a), then f is strictly monotone on α.

Русский

Если для каждого a, не максимального, выполняется f(a) < f(succ(a)), то функция f строго монотонна на α.

LaTeX

$$$\\Big( \\forall a, \\neg \\operatorname{IsMax}(a) \\to f(a) < f(\\operatorname{succ}(a)) \\Big) \\to \\operatorname{StrictMono}(f).$$$

Lean4

theorem strictMono_of_lt_succ (hf : ∀ a, ¬IsMax a → f a < f (succ a)) : StrictMono f := by
  simpa using strictMonoOn_of_lt_succ Set.ordConnected_univ (by simpa using hf)

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