English
A function f is antitone iff for every s and every a not in s, f(insert a s) ≤ f s.
Русский
Функция f антитонна тогда и только тогда, когда для каждого s и каждого a ∉ s выполняется f(insert a s) ≤ f s.
LaTeX
$$$\\text{Antitone}(f) \\iff \\forall s, \\forall a; a \\notin s \\to f(\\mathrm{insert}\\ a\\ s) \\le f(s)$$$
Lean4
/-- A function `f` from `Finset α` is antitone if and only if `f (insert a s) ≤ f s` for all
`s` and `a ∉ s`. -/
theorem antitone_iff_forall_insert_le : Antitone f ↔ ∀ s ⦃a⦄, a ∉ s → f (insert a s) ≤ f s :=
monotone_iff_forall_le_insert (β := βᵒᵈ)