mem_top_objs

Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

English

Every object c is contained in the objects of the top subgroupoid.

Русский

Каждый объект содержится в множествах объектов верхней подгруппоида.

LaTeX

$$c ∈ (⊤ : Subgroupoid C).objs$$

Lean4

theorem mem_top_objs (c : C) : c ∈ (⊤ : Subgroupoid C).objs :=
  by
  dsimp [Top.top, objs]
  simp only [univ_nonempty]

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

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

Разделы

Аффилиация

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