antitone_dual_iff — Mathlib

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]

Похожие утверждения