English
A unified statement that Antitone via the dual equals Antitone after dualization: Antitone (toDual ∘ f ∘ ofDual) ↔ Antitone f.
Русский
Обобщённое утверждение: антитонность через двойственной порядок равносильна антитонности после двойственного отображения.
LaTeX
$$$\operatorname{Antitone}(\mathrm{toDual} \circ f \circ \mathrm{ofDual}) \iff \operatorname{Antitone}(f)$$$
Lean4
theorem antitone_dual_iff : Antitone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ Antitone f := by
rw [antitone_toDual_comp_iff, monotone_comp_ofDual_iff]