generated_le_generatedNormal

Mathlib.CategoryTheory.Groupoid.Subgroupoid

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

English

The normal subgroupoid generated by X is itself normal.

Русский

Порожденная по X нормальная подпогруппоида сама нормальна.

LaTeX

$$$(generatedNormal X).IsNormal$$$

Lean4

theorem generated_le_generatedNormal : generated X ≤ generatedNormal X :=
  by
  apply @sInf_le_sInf (Subgroupoid C) _
  exact fun S ⟨h, _⟩ => h

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

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

Разделы

Аффилиация

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