Icc_inl_inr — Mathlib

English

In Lex, the closed interval from a left-embedded to a right-embedded element equals the image of the disjoint sum of principal intervals mapped via toLex.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Icc_inl_inr : Icc (inlₗ a) (inrₗ b) = ((Ici a).disjSum (Iic b)).map toLex.toEmbedding :=
  rfl

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