instIsEmptyDiscrete — Mathlib

English

If α is an empty type, then the discrete category on α is empty as a category; i.e. there are no objects or morphisms.

Русский

Если α пустой тип, то дискретная категория на α пустая как категория; т. е. объектов и морфизмов нет.

LaTeX

$$$\operatorname{IsEmpty}(\mathrm{Discrete}\, \alpha) \text{ if } \mathrm{IsEmpty}(\alpha)$$$

Lean4

instance (α : Type*) [IsEmpty α] : IsEmpty (Discrete α) :=
  Function.isEmpty Discrete.as

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