toLocallyFiniteOrderTop — Mathlib

English

An empty type is locally finite in the top sense.

Русский

Пустой тип локально конечен сверху.

LaTeX

$$$\text{IsEmpty}(\alpha) \Rightarrow \text{LocallyFiniteOrderTop}(\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 toLocallyFiniteOrderTop [Preorder α] [IsEmpty α] : LocallyFiniteOrderTop α
    where
  finsetIci := isEmptyElim
  finsetIoi := isEmptyElim
  finset_mem_Ici := isEmptyElim
  finset_mem_Ioi := isEmptyElim

Похожие утверждения