Ioc_ofDual — Mathlib

English

In the dual order, a half-open interval from a to b corresponds to the opposite half-open interval in the original order mapped via the embedding.

Русский

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

LaTeX

$$$ Ioc (ofDual a) (ofDual b) = (Ico b a).map ofDual.toEmbedding $$$

Lean4

theorem Ioc_ofDual (a b : αᵒᵈ) : Ioc (ofDual a) (ofDual b) = (Ico b a).map ofDual.toEmbedding :=
  map_refl.symm

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