instObjAsType

Mathlib.CategoryTheory.Countable

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CountableCategory.instObjAsType

English

Given α with a countable category structure, CountableCategory (ObjAsType α) holds, i.e., the category of objects represented by α is countable.

Русский

Пусть α имеет счетную категорию; тогда CountableCategory (ObjAsType α).

LaTeX

$$$ \\operatorname{CountableCategory}(\\mathrm{ObjAsType}(\\alpha)) $$$

Lean4

instance : CountableCategory (ObjAsType α) where

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

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

Разделы

Аффилиация

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