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