English
In the lexicographic sum α ⊕β, the open lower interval below inl a consists exactly of all inl x with x < a; no inr elements lie strictly below inl a in the Lex order. Thus Iio(inl a) corresponds to the image of Iio a under the left embedding.
Русский
В лексикографическом суммировании α ⊕ β множество элементов, меньших по отношению к inl a, состоит только из элементов inl x с x < a; элементы типа inr не лежат строго ниже inl a в этом порядке. Следовательно Iio(inl a) является образом Iio a через левое вложение.
LaTeX
$$$ I\\!io\\,\\bigl(\\mathrm{inl}_{\\ell}\\, a\\bigr) = \\bigl(Iio\\, a\\bigr).\\mathrm{map} \\, (\\mathrm{Embedding.inl}.trans\\, \\mathrm{toLex.toEmbedding}) $$$
Lean4
theorem Iio_inl : Iio (inlₗ a : α ⊕ₗ β) = (Iio a).map (Embedding.inl.trans toLex.toEmbedding) :=
rfl
