English
If α and β are locally finite orders with a top element, then the disjoint sum α ⊕ β equipped with the natural top order is locally finite, and its principal upper and lower sets are obtained by mapping the corresponding upper/lower sets from each summand into the sum via the natural injections.
Русский
Если α и β — локально конечные порядки с верхним элементом, то их попарное сумма α ⊕ β, снабженная естественным верхним порядком, также локально конечна; окрестности верхних и нижних пределов получаются как отображения соответствующих множеств из каждой составляющей через естественные вложения.
LaTeX
$$$ \text{LocallyFiniteOrderTop}(\alpha \oplus \beta) \text{ с } \text{finsetIci} = \mathrm{Sum.elim}(\mathrm{Ici} \cdot |>.map \mathrm{.inl})(\mathrm{Ici} \cdot |>.map \mathrm{inr})$ и аналогично для finsetIoi.$$
Lean4
instance : LocallyFiniteOrderTop (α ⊕ β)
where
finsetIci := Sum.elim (Ici · |>.map .inl) (Ici · |>.map .inr)
finsetIoi := Sum.elim (Ioi · |>.map .inl) (Ioi · |>.map .inr)
finset_mem_Ici := by simp
finset_mem_Ioi := by simp
