disconnect_objs

Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

English

The set of objects of the disconnect subgroupoid equals the set of objects of the original subgroupoid.

Русский

Множество объектов подгруппоида disconnect равно множеству объектов исходного подгруппоида.

LaTeX

$$$S.disconnect.objs = S.objs$$$

Lean4

theorem disconnect_objs : S.disconnect.objs = S.objs :=
  Set.ext fun _ ↦ mem_disconnect_objs_iff _

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

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

Разделы

Аффилиация

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