Ioo_inr_inl — Mathlib

English

In Lex, the open interval between two right-embedded elements maps to the image of the interval (Ioi a) disjSum (Iio b) under toLex embeddings.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ioo_inr_inl : Ioo (inrₗ b) (inlₗ a) = ∅ :=
  rfl

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