Iic_ofDual — Mathlib

English

Let α be a preorder. For any x ∈ αᵒᵈ, the interval [ofDual x, ∞) in the dual order is the preimage under the duality map of [−∞, x] in the original order.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Iic_ofDual {x : αᵒᵈ} : Iic (ofDual x) = toDual ⁻¹' Ici x :=
  rfl

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