Ioo_toDual — Mathlib

English

Let α be a preorder. For any a,b ∈ α, the open interval (toDual a, toDual b) in the dual order is the preimage under the duality map of the open interval (b, a) in the original order.

Русский

Пусть α — предпорядок. Для любых a, b ∈ α открытый интервал (toDual a, toDual b) во втором порядке равен прообразу открытого интервала (b, a) в исходном порядке по двойственной точке.

LaTeX

$$$$ \\mathrm{Ioo}(\\mathrm{toDual}(a), \\mathrm{toDual}(b)) = \\mathrm{toDual}^{-1}\\!\\'\\'\\mathrm{Ioo}(b, a). $$$$

Lean4

@[simp]
theorem Ioo_toDual : Ioo (toDual a) (toDual b) = ofDual ⁻¹' Ioo b a :=
  Set.ext fun _ => and_comm

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