Ioi_ofDual — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ioi_ofDual {x : αᵒᵈ} : Ioi (ofDual x) = toDual ⁻¹' Iio x :=
  rfl

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