Ici_ofDual — Mathlib

English

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

Русский

Пусть α — предпорядок. Для любого x ∈ αᵒᵈ интервал [ofDual x, ∞) во втором порядке равен прообразу [−∞, x] в исходном порядке по двойственной отображению.

LaTeX

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

Lean4

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

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