toProfiniteObj

Mathlib.Topology.Category.Profinite.Basic

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

Lean4

/-- (Implementation) The object part of the connected_components functor from compact Hausdorff spaces
to Profinite spaces, given by quotienting a space by its connected components. -/
@[stacks 0900]
def toProfiniteObj (X : CompHaus.{u}) : Profinite.{u}
    where
  toTop := TopCat.of (ConnectedComponents X)
  is_compact := Quotient.compactSpace
  is_hausdorff := ConnectedComponents.t2
  prop := ConnectedComponents.totallyDisconnectedSpace

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

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

Разделы

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

Аффилиация

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