strictMono_iff_forall_lt_insert — Mathlib

English

A function f is strictly monotone iff for all s and a not in s, f(s) < f(insert a s).

Русский

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

LaTeX

$$$\\text{StrictMono}(f) \\iff ∀ s, ∀ a, a \\notin s \\to f(s) < f(\\mathrm{insert}\\ a\\ s)$$$

Lean4

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

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