instPreregular

Mathlib.Topology.Category.LightProfinite.EffectiveEpi

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

English

LightProfinite is preregular.

Русский

LightProfinite является пререгулярной категорией.

LaTeX

$$$\text{Preregular}(\mathrm{LightProfinite})$$$

Lean4

instance : Preregular LightProfinite.{u} := by
  apply CompHausLike.preregular
  intro _ _ f
  exact (effectiveEpi_iff_surjective f).mp

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

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

Разделы

Аффилиация

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