English
In the Lex sum, the upper interval Ici(inl a) is the image of Ici(a) together with all right components; more precisely, Ici(inl a) equals the embedding of (Ici a) disjoint-summed with univ.
Русский
В лексикографической сумме верхний интервал над inl a состоит из образа Ici(a) совместно со всем правым компонентам; точнее, Ici(inl a) равняется отображению (Ici a) через дисж-сумму с единичным множеством.
LaTeX
$$$ Ici\\bigl(\\mathrm{inl}_{\\ell}\\, a\\bigr) = \\bigl((\\mathrm{Ici}\\, a) \\disjSum \\mathrm{univ}\\bigr).\\mathrm{map}\\;\\mathrm{toLex.toEmbedding}$$$
Lean4
theorem Ici_inl : Ici (inlₗ a : α ⊕ₗ β) = ((Ici a).disjSum Finset.univ).map toLex.toEmbedding :=
rfl
