English
If α is a preorder and α is empty, then α carries a LocallyFiniteOrderBot structure; in particular, every interval is finite (indeed empty).
Русский
Пусть α — множество с отношением порядка, и α пусто. Тогда на α существует структура LocallyFiniteOrderBot; в частности, каждый интервал существенно конечен (на самом деле пуст).
LaTeX
$$$\operatorname{IsEmpty}(\alpha) \Rightarrow \operatorname{LocallyFiniteOrderBot}(\alpha)$$$
Lean4
/-- An empty type is locally finite.
This is not an instance as it would not be defeq to more specific instances. -/
protected abbrev toLocallyFiniteOrderBot [Preorder α] [IsEmpty α] : LocallyFiniteOrderBot α
where
finsetIic := isEmptyElim
finsetIio := isEmptyElim
finset_mem_Iic := isEmptyElim
finset_mem_Iio := isEmptyElim
