English
In the lexicographic sum α ⊕ β, the open lower interval below inr b consists of all elements with left component arbitrary and right component strictly less than b; i.e., Iio(inr b) is the image of (Iio b) under the right embedding.
Русский
В лексикографическом суммировании α ⊕ β множество элементов, меньших чем inr b, состоит из всех элементов, имеющих произвольную левую часть и правую часть строго меньшую b; то есть Iio(inr b) есть образ Iio b при правом вложении.
LaTeX
$$$ I\\!io\\,\\bigl(\\mathrm{inr}_{\\ell}\\, b\\bigr) = \\bigl(Iio\\, b\\bigr).\\mathrm{map} \\, \\mathrm{toLex.toEmbedding} $$$
Lean4
theorem Iio_inr : Iio (inrₗ b : α ⊕ₗ β) = (Finset.univ.disjSum (Iio b)).map toLex.toEmbedding :=
rfl
