Ioc_inr_inr — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem Ioc_inr_inr : Ioc (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Ioc b₁ b₂).map (Embedding.inr.trans toLex.toEmbedding) := by
  rw [← Finset.map_map]; rfl

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