toLocallyFiniteOrder — Mathlib

English

An empty type is locally finite.

Русский

Пустой тип является локально конечным порядком.

LaTeX

$$$\text{IsEmpty}(\alpha) \Rightarrow \text{LocallyFiniteOrder}(\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 toLocallyFiniteOrder [Preorder α] [IsEmpty α] : LocallyFiniteOrder α
    where
  finsetIcc := isEmptyElim
  finsetIco := isEmptyElim
  finsetIoc := isEmptyElim
  finsetIoo := isEmptyElim
  finset_mem_Icc := isEmptyElim
  finset_mem_Ico := isEmptyElim
  finset_mem_Ioc := isEmptyElim
  finset_mem_Ioo := isEmptyElim

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