antitoneOn_dual_iff — Mathlib

English

For any α, β with preorders and f, and subset s, AntitoneOn (toDual ∘ f ∘ ofDual) s is equivalent to AntitoneOn f s.

Русский

Для любых $\alpha, \beta$ и подмножества $s$ антитонность через двойной порядок совпадает с антитонностью на исходном.

LaTeX

$$$\operatorname{AntitoneOn}(\mathrm{toDual} \circ f \circ \mathrm{ofDual}, s) \iff \operatorname{AntitoneOn}(f, s)$$$

Lean4

theorem antitoneOn_dual_iff : AntitoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ AntitoneOn f s := by
  rw [antitoneOn_toDual_comp_iff, monotoneOn_comp_ofDual_iff]

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