monotone_dual_iff — Mathlib

English

A unified statement that Monotone via the dual equals Monotone after dualization: Monotone (toDual ∘ f ∘ ofDual) ↔ Monotone f.

Русский

Обобщённое утверждение: монотонность через двойственный порядок равносильна монотонности после двойственного отображения.

LaTeX

$$$\operatorname{Monotone}(\mathrm{toDual} \circ f \circ \mathrm{ofDual}) \iff \operatorname{Monotone}(f)$$$

Lean4

theorem monotone_dual_iff : Monotone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ Monotone f := by
  rw [monotone_toDual_comp_iff, antitone_comp_ofDual_iff]

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