monotone_of_pred_le — Mathlib

English

If for all a with not IsMin a we have f(pred a) ≤ f a, then f is monotone.

Русский

Если для каждого a, не минимального, выполняется f(pred a) ≤ f(a), то f монотонна.

LaTeX

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

Lean4

theorem monotone_of_pred_le (hf : ∀ a, ¬IsMin a → f (pred a) ≤ f a) : Monotone f := by
  simpa using monotoneOn_of_pred_le Set.ordConnected_univ (by simpa using hf)

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