English
In the Lex sum, the Ioi (inl a) consists of all inl a′ with a < a′ together with all inr b, reflecting that any inr element is larger than any inl element in the Lex order.
Русский
В лексикографической сумме Ioi(inl a) содержит все inl a′ с a < a′ и все элементы inr b, поскольку любой inr бóльше любого inl в этом порядке.
LaTeX
$$$ Ioi\\bigl(\\mathrm{inl}_{\\ell}\\, a\\bigr) = \\bigl((\\Ioi\\, a) \\disjSum \\mathrm{univ}\\bigr).\\mathrm{map}\\;\\mathrm{toLex.toEmbedding}$$$
Lean4
theorem Ioi_inl : Ioi (inlₗ a : α ⊕ₗ β) = ((Ioi a).disjSum Finset.univ).map toLex.toEmbedding :=
rfl