strictMono_iff_forall_lt_cons — Mathlib

English

A function f is strictly monotone if and only if for every s and every a not in s, f(s) < f(cons a s ha).

Русский

Функция f строго монотонна тогда и только тогда, когда для каждого s и каждого a ∉ s выполняется f(s) < f(cons a s ha).

LaTeX

$$$\\text{StrictMono}(f) \\iff \\forall s, \\forall a\\; ha, f(s) < f(\\mathrm{cons}\\, a\, s\, ha)$$$

Lean4

/-- A function `f` from `Finset α` is strictly monotone if and only if `f s < f (cons a s ha)` for
all `s` and `a ∉ s`. -/
theorem strictMono_iff_forall_lt_cons : StrictMono f ↔ ∀ s ⦃a⦄ ha, f s < f (cons a s ha) := by
  classical simp [strictMono_iff_forall_covBy, covBy_iff_exists_cons]

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