countableCategoryDiscreteOfCountable

Mathlib.CategoryTheory.Countable

URI: https://scilib.ai/kg/mathlib#CategoryTheory.countableCategoryDiscreteOfCountable

English

Same statement as above, establishing countability of Discrete α for any countable α.

Русский

То же утверждение: дискретная категория на α счетна для любого счетного α.

LaTeX

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

Lean4

instance countableCategoryDiscreteOfCountable (J : Type*) [Countable J] : CountableCategory (Discrete J) where

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

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

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru