presentation

Mathlib.Topology.Category.Stonean.Basic

URI: https://scilib.ai/kg/mathlib#CompHaus.presentation

Lean4

/-- If `X` is compact Hausdorff, `presentation X` is a Stonean space equipped with an epimorphism
  down to `X` (see `CompHaus.presentation.π` and `CompHaus.presentation.epi_π`). It is a
  "constructive" witness to the fact that `CompHaus` has enough projectives. -/
noncomputable def presentation (X : CompHaus) : Stonean
    where
  toTop := (projectivePresentation X).p.1
  prop := instExtremallyDisconnectedCarrierToTopTrueOfProjective X.projectivePresentation.p

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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