English
If α and β are locally finite orders, then the disjoint sum α ⊕ β can be equipped with a locally finite order, with finitary intervals defined via sumLift₂ using Icc, Ico, Ioc, Ioo on each component.
Русский
Пусть α и β — локально конечные порядки; их поразностное объединение α ⊕ β можно наделить локально конечным порядком, интервалы Icc, Ico, Ioc, Ioo определяются через lift₂ и соответствующие интервалы на компонентах.
LaTeX
$$$\text{LocallyFiniteOrder}(\alpha \oplus \beta) \quad \text{with} \quad \mathrm{finsetIcc} = \mathrm{sumLift_2}(\mathrm{Icc},\mathrm{Icc}), \mathrm{finsetIco} = \mathrm{sumLift_2}(\mathrm{Ico},\mathrm{Ico}), \mathrm{finsetIoc} = \mathrm{sumLift_2}(\mathrm{Ioc},\mathrm{Ioc}), \mathrm{finsetIoo} = \mathrm{sumLift_2}(\mathrm{Ioo},\mathrm{Ioo}).$$$
Lean4
instance instLocallyFiniteOrder : LocallyFiniteOrder (α ⊕ β)
where
finsetIcc := sumLift₂ Icc Icc
finsetIco := sumLift₂ Ico Ico
finsetIoc := sumLift₂ Ioc Ioc
finsetIoo := sumLift₂ Ioo Ioo
finset_mem_Icc := by simp
finset_mem_Ico := by simp
finset_mem_Ioc := by simp
finset_mem_Ioo := by simp
