instIsGroupoidOfIsDiscrete

Mathlib.CategoryTheory.Groupoid.Discrete

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

English

If C is a discrete category, then C is a groupoid (every morphism is invertible).

Русский

Если C — дискретная категория, то она является групоидом: все морфизмы обратимы.

LaTeX

$$$\\text{IsGroupoid}(C)$ при условии, что $C$ дискретна$$

Lean4

instance [Category C] [IsDiscrete C] : IsGroupoid C where

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

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

Разделы

Аффилиация

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