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