mem_top

Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

English

Any arrow f: c → d belongs to the arrows of the top subgroupoid, i.e., the ambient arrow set.

Русский

Любая стрелка f: c → d принадлежит стрелам верхней подгруппоида, то есть множеству стрел исходного группоида.

LaTeX

$$f ∈ (⊤ : Subgroupoid C).arrows c d$$

Lean4

theorem mem_top {c d : C} (f : c ⟶ d) : f ∈ (⊤ : Subgroupoid C).arrows c d :=
  trivial

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

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

Разделы

Аффилиация

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