monotone_of_le_succ — Mathlib

English

If for all a with a not maximal we have f(a) ≤ f(succ a), then f is monotone on the entire α.

Русский

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

LaTeX

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

Lean4

theorem monotone_of_le_succ (hf : ∀ a, ¬IsMax a → f a ≤ f (succ a)) : Monotone f := by
  simpa using monotoneOn_of_le_succ Set.ordConnected_univ (by simpa using hf)

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