disconnect_isTotallyDisconnected

Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

English

The disconnect of a subgroupoid is totally disconnected.

Русский

Подгруппа disconnect полностью разобщена.

LaTeX

$$$S.disconnect.IsTotallyDisconnected$$$

Lean4

theorem disconnect_isTotallyDisconnected : S.disconnect.IsTotallyDisconnected := by rw [isTotallyDisconnected_iff];
  exact fun c d ⟨_, h, _⟩ => h

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

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

Разделы

Аффилиация

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