id_mem

Mathlib.CategoryTheory.Groupoid.Subgroupoid

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subgroupoid.IsWide.id_mem

English

If S is wide, then for every c, the identity id_c belongs to S.arrows c c.

Русский

Если S широка, то для каждого узла c тождественный морфизм id_c принадлежит S.arrows c c.

LaTeX

$$Sw.wide ⇒ ∀ c, 𝟙_c ∈ S.arrows c c$$

Lean4

theorem id_mem {S : Subgroupoid C} (Sw : S.IsWide) (c : C) : 𝟙 c ∈ S.arrows c c :=
  Sw.wide c

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

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

Разделы

Аффилиация

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