English
Let α be a preorder. For any a,b ∈ α, the closed interval between toDual a and toDual b in the dual order equals the preimage under the duality map of the closed interval between b and a in the original order.
Русский
Пусть α — предпорядок. Для любых a, b ∈ α замкнутый интервал между toDual a и toDual b во втором порядке равен прообразу двойственной отображения замкнутого интервала между b и a в исходном порядке.
LaTeX
$$$$ \\mathrm{Icc}(\\mathrm{toDual}(a), \\mathrm{toDual}(b)) = \\mathrm{ofDual}^{-1}\\'\\'\\mathrm{Icc}(b, a). $$$$
Lean4
@[simp]
theorem Icc_toDual : Icc (toDual a) (toDual b) = ofDual ⁻¹' Icc b a :=
Set.ext fun _ => and_comm
