Ioo_ofDual — Mathlib

English

In the dual order, the open interval between a and b is the image under the embedding of the open interval between b and a in the original order.

Русский

В двойственном порядке открытый интервал между a и b является образом открытого интервала между b и a в исходном порядке.

LaTeX

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

Lean4

theorem Ioo_ofDual (a b : αᵒᵈ) : Ioo (ofDual a) (ofDual b) = (Ioo b a).map ofDual.toEmbedding :=
  map_refl.symm

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