Ioc_toDual — Mathlib

English

Let α be a preorder. For any a,b ∈ α, the half-open interval (a, b] in the dual order corresponds to the preimage of the half-open interval (b, a] in the original order under the duality map.

Русский

Пусть α — предпорядок. Для любых a, b ∈ α полуоткрытый интервал (a, b] во втором порядке соответствует прообразу полуоткрытого интервала (b, a] в исходном порядке по отображению двойственности.

LaTeX

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

Lean4

@[simp]
theorem Ioc_toDual : Ioc (toDual a) (toDual b) = ofDual ⁻¹' Ico b a :=
  Set.ext fun _ => and_comm

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