antitone_iff_forall_cons_le — Mathlib

English

A function f is antitone if and only if for every s and every a not in s, f(cons a s ha) ≤ f s.

Русский

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

LaTeX

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

Lean4

/-- A function `f` from `Finset α` is antitone if and only if `f (cons a s ha) ≤ f s` for all
`s` and `a ∉ s`. -/
theorem antitone_iff_forall_cons_le : Antitone f ↔ ∀ s ⦃a⦄ ha, f (cons a s ha) ≤ f s :=
  monotone_iff_forall_le_cons (β := βᵒᵈ)

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