Ico_ofDual — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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