monotone_iff_forall_le_cons — Mathlib

English

A function f from Finset α to a preordered set is monotone if and only if for every s and every a not in s, f(s) ≤ f(cons a s ha).

Русский

Функция f от Finset α к упорядоченному множеству монотонна тогда и только тогда, когда для каждого множества s и для любого элемента a, не принадлежащего s, выполняется f(s) ≤ f(s ∪ {a}).

LaTeX

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

Lean4

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

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