disconnect_le

Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

English

Thedisconnect construction of a subgroupoid S is contained in S itself; i.e., every arrow and object in S.disconnect also lies in S.

Русский

Конструкция disconnect подгруппоида S содержится в самом S: каждый объект и стрелка в S.disconnect принадлежит S.

LaTeX

$$$S.disconnect \\le S$$$

Lean4

theorem disconnect_le : S.disconnect ≤ S := by rw [le_iff]; rintro _ _ _ ⟨⟩; assumption

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

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

Разделы

Аффилиация

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