Icc_inr_inl — Mathlib

English

In Lex, the closed interval from a right-embedded to a left-embedded element equals the image of (Ici a).disjSum (Iic b) under toLex embeddings.

Русский

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

LaTeX

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

Lean4

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

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