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