discreteCountable — Mathlib

English

If α is a type with a countable structure, then the discrete category on α is countable as a category.

Русский

Если α имеет счетную структуру, то дискретная категория на α является счетной как категория.

LaTeX

$$$ \\operatorname{Countable}(\\mathrm{Discrete}(\\alpha)) $$$

Lean4

instance discreteCountable {α : Type*} [Countable α] : Countable (Discrete α) :=
  Countable.of_equiv α discreteEquiv.symm

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