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