Ioo_inl_inr — Mathlib

English

In Lex, the open interval from a left-embedded to a right-embedded element equals the image of (Ioi a) disjoint sum (Iio b) under toLex embeddings.

Русский

В Lex открытый интервал между левым и правым встроенными элементами равен образу (Ioi a) disjSum (Iio b) через встраивания toLex.

LaTeX

$$$ \operatorname{Ioo}(\mathrm{inl}_\ell a)(\mathrm{inr}_\ell b) = ((\mathrm{Ioi} a).\mathrm{disjSum}(\mathrm{Iio} b)).\mathrm{map} toLex.toEmbedding $$$

Lean4

@[simp]
theorem Ioo_inl_inr : Ioo (inlₗ a) (inrₗ b) = ((Ioi a).disjSum (Iio b)).map toLex.toEmbedding :=
  rfl

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