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