English
In the Lexicographic sum, the closed interval from a left-embedded element to a right-embedded element corresponds to the sum of principal intervals mapped into the Lex sum.
Русский
В лексикографической сумме замкнутый интервал от левого встроенного к правому встроенному соответствует сумме соответствующих интервалов, отображённых в Lex.
LaTeX
$$$ \operatorname{Icc}(\mathrm{inl}_\ell a)(\mathrm{inr}_\ell b) = (\operatorname{Ici} a).\mathrm{disjSum}(\operatorname{Iic} b) \;\mathrm{.map}\; toLex.toEmbedding $$$
Lean4
theorem Icc_inl_inl : Icc (inlₗ a₁ : α ⊕ₗ β) (inlₗ a₂) = (Icc a₁ a₂).map (Embedding.inl.trans toLex.toEmbedding) := by
rw [← Finset.map_map]; rfl
