Ico_inl_inr — Mathlib

English

In Lex, the half-open interval from a left-embedded to a right-embedded element is the image of the corresponding principal interval under toLex embeddings.

Русский

В Lex полупромежуток между левым и правым встроенными элементами равен образу соответствующего интервала через встраивания toLex.

LaTeX

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

Lean4

@[simp]
theorem Ico_inl_inr : Ico (inlₗ a) (inrₗ b) = ((Ici a).disjSum (Iio b)).map toLex.toEmbedding :=
  rfl

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