Icc_ofDual — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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