English
In the Lex sum, the Ioi(inr b) consists exactly of all inr b′ with b < b′; there are no left components strictly larger than inr b since all inl elements are below any inr element in Lex.
Русский
В лексикографической сумме Ioi(inr b) состоит только из элементов inr b′ с b < b′; левый компонент не может быть выше inr b, так как все inl-множества ниже любого inr-элемента.
LaTeX
$$$ Ioi\\bigl(\\mathrm{inr}_{\\ell}\\, b\\bigr) = \\bigl((\\Ioi\\, b) \\disjSum \\mathrm{univ}\\bigr).\\mathrm{map}\\;\\mathrm{toLex.toEmbedding}$$$
Lean4
theorem Ioi_inr : Ioi (inrₗ b : α ⊕ₗ β) = (Ioi b).map (Embedding.inr.trans toLex.toEmbedding) :=
rfl
