strictMono_dual_iff — Mathlib

English

Theorem: StrictMono (toDual ∘ f ∘ ofDual) ↔ StrictMono f.

Русский

Теорема: строгая монотонность через двойственный порядок равносильна строгой монотонности на исходном порядке.

LaTeX

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

Lean4

theorem strictMono_dual_iff : StrictMono (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictMono f := by
  rw [strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff]

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