English
Let α be a locally finite preorder and β a preorder. A function f: α → β is StrictAnti iff it is strictly antitone on all cover relations, i.e., for every a,b with a ⋖ b we have f(b) < f(a).
Русский
Пусть α — локально конечный предпорядок, β — предпорядок. Функция f: α → β строго антитонна тогда и только тогда, когда для всех a,b с a ⋖ b выполняется f(b) < f(a).
LaTeX
$$$\operatorname{StrictAnti}(f) \iff \forall a,b\in \alpha\, (a \prec b) \Rightarrow f(b) < f(a)$$$
Lean4
/-- A function from a locally finite preorder is strictly antitone if and only if it is strictly
antitone when restricted to pairs satisfying `a ⋖ b`. -/
theorem strictAnti_iff_forall_covBy [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) :
StrictAnti f ↔ ∀ a b : α, a ⋖ b → f b < f a :=
strictMono_iff_forall_covBy (β := βᵒᵈ) f
