instPreregular

Mathlib.Topology.Category.Profinite.EffectiveEpi

URI: https://scilib.ai/kg/mathlib#Profinite.instPreregular

English

The Profinite category is preregular, inherited from its compact Hausdorff reflection.

Русский

Категория Profinite прeregular; переход от Profinite к CompHaus сохраняет прегрегулярность.

LaTeX

$$$\mathrm{Preregular}(\mathrm{Profinite})$$$

Lean4

instance : Preregular Profinite.{u} :=
  profiniteToCompHaus.reflects_preregular

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

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

Разделы

Аффилиация

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