English
Let α and β be preordered sets with a bottom element (locally finite with bottom). Then for every b ∈ β, the set of elements of α ⊕ β strictly less than inr b corresponds exactly to the right-embedded image of the interval Iio(b) into α ⊕ β.
Русский
Пусть α и β образуют упорядоченные множества с нижним элементом и свойствами локальной конечноценности. Тогда для любого b ∈ β множество элементов α ⊕ β, строго меньших чем inr b, совпадает с отображением через встроение inr образа интервала Iio(b) в α ⊕ β.
LaTeX
$$$ \operatorname{Iio}(\mathrm{inr}\, b) = \mathrm{map}(\mathrm{Embedding.inr})(\operatorname{Iio} b) $$$
Lean4
theorem Iio_inr : Iio (inr b : α ⊕ β) = (Iio b).map Embedding.inr :=
rfl
