Ioc_ofDual — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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