Ioo_toDual — Mathlib

English

Let α be a preorder with locally finite intervals. For any a,b in α, the open interval between a and b in the dual order corresponds to the image, under the natural embedding, of the open interval between b and a in α.

Русский

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

LaTeX

$$$ Ioo (toDual a) (toDual b) = (Ioo b a).map toDual.toEmbedding $$$

Lean4

theorem Ioo_toDual : Ioo (toDual a) (toDual b) = (Ioo b a).map toDual.toEmbedding :=
  map_refl.symm

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