Iio_toDual — Mathlib

English

Let α be a preorder. For any a ∈ α, the open interval below a in the dual order coincides with the preimage under the duality map of the open interval above a in the original order.

Русский

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

LaTeX

$$$$ \\mathrm{Iio}(\\mathrm{toDual}(a)) = \\mathrm{ofDual}^{-1}\\'\\'\\mathrm{Ioi}(a). $$$$

Lean4

@[simp]
theorem Iio_toDual : Iio (toDual a) = ofDual ⁻¹' Ioi a :=
  rfl

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