Ioc_inl_inr — Mathlib

English

In Lex, the half-open interval from a left-embedded to a right-embedded element is the image of the sum of Ioi a and Iic b under toLex embeddings.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ioc_inl_inr : Ioc (inlₗ a) (inrₗ b) = ((Ioi a).disjSum (Iic b)).map toLex.toEmbedding :=
  rfl

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