strictMono_of_pred_lt — Mathlib

English

If for all a not minimal with a ∈ s and pred a ∈ s we have f(pred a) < f a, then StrictMonoOn f s.

Русский

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

LaTeX

$$$\\operatorname{OrdConnected}(s) \\to \\Big( \\forall a, \\neg \\operatorname{IsMin}(a) \\to a \\in s \\to \\operatorname{pred}(a) \\in s \\to f(\\operatorname{pred}(a)) < f(a) \\Big) \\to \\operatorname{StrictMonoOn}(f,s).$$$

Lean4

theorem strictMono_of_pred_lt (hf : ∀ a, ¬IsMin a → f (pred a) < f a) : StrictMono f := by
  simpa using strictMonoOn_of_pred_lt Set.ordConnected_univ (by simpa using hf)

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