monotone_iff_forall_le_insert — Mathlib

English

A function f is monotone iff for every s and every a not in s, f(s) ≤ f(insert a s).

Русский

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

LaTeX

$$$\\text{Monotone}(f) \\iff \\forall s, \\forall a, a \\notin s \\to f(s) \\le f(\\mathrm{insert}\\ a\\ s)$$$

Lean4

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

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