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