instIsLocallyDiscreteLocallyDiscrete

Mathlib.CategoryTheory.Bicategory.LocallyDiscrete

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Bicategory.instIsLocallyDiscreteLocallyDiscrete

English

For any category C, the LocallyDiscrete C is locally discrete.

Русский

Для любой категории C локально-дискретное C является локально дискретным.

LaTeX

$$$\\forall C, [\\text{Category } C] : IsLocallyDiscrete(\\text{LocallyDiscrete } C).$$$

Lean4

instance (C : Type*) [Category C] : IsLocallyDiscrete (LocallyDiscrete C) := fun _ _ ↦ Discrete.isDiscrete _

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

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

Разделы

Аффилиация

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