English
A function f is strictly 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{StrictAnti}(f) \\iff \\forall s, \\forall a; ha, f(\\mathrm{cons}\\, a\, s\, ha) < f(s)$$$
Lean4
/-- A function `f` from `Finset α` is strictly antitone if and only if `f (cons a s ha) < f s` for
all `s` and `a ∉ s`. -/
theorem strictAnti_iff_forall_cons_lt : StrictAnti f ↔ ∀ s ⦃a⦄ ha, f (cons a s ha) < f s :=
strictMono_iff_forall_lt_cons (β := βᵒᵈ)