English
In Lex, the half-open interval between two right-embedded elements maps to the image of the corresponding half-open interval in β under the right embedding composed with toLex.
Русский
В Lex полупрерыв между двумя правыми встроенными элементами отображается как образ соответствующего полупериода в β через встроение inr и toLex.
LaTeX
$$$ \operatorname{Ico}(\mathrm{inr}_\ell b_1)(\mathrm{inr}_\ell b_2) = (\operatorname{Ico} b_1 b_2).\mathrm{map}(\mathrm{Embedding.inr} .\mathrm{trans} toLex.toEmbedding) $$$
Lean4
theorem Ico_inr_inr : Ico (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Ico b₁ b₂).map (Embedding.inr.trans toLex.toEmbedding) := by
rw [← Finset.map_map]; rfl
