Ioo_ofDual — Mathlib

English

Let α be a preorder. For any x,y ∈ αᵒᵈ, the open interval Ioo (toDual y) (toDual x) in the dual order equals the preimage under the duality map of Ioo x y in the original order.

Русский

Пусть α — предпорядок. Для любых x,y ∈ αᵒᵈ открытый интервал Ioo (toDual y) (toDual x) во втором порядке равен прообразу Ioo x y под двойственным отображением.

LaTeX

$$$$ \\mathrm{Ioo}(\\mathrm{toDual}(y), \\mathrm{toDual}(x)) = \\mathrm{toDual}^{-1}\\'\\'\\mathrm{Ioo}(x, y). $$$$

Lean4

@[simp]
theorem Ioo_ofDual {x y : αᵒᵈ} : Ioo (ofDual y) (ofDual x) = toDual ⁻¹' Ioo x y :=
  Set.ext fun _ => and_comm

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