English
Let α be a locally finite preorder. For a,b in αᵒᵈ, the closed interval from a to b in the dual equals the image of the closed interval from b to a in α under the embedding.
Русский
Пусть α — локально конечный предорядок. Для a,b ∈ αᵒᵈ замкнутый интервал между a и b в двойственном порядке равен образу замкнутого интервала между b и a в α под вложением.
LaTeX
$$$ Icc (ofDual a) (ofDual b) = (Icc b a).map ofDual.toEmbedding $$$
Lean4
theorem Icc_ofDual (a b : αᵒᵈ) : Icc (ofDual a) (ofDual b) = (Icc b a).map ofDual.toEmbedding :=
map_refl.symm