Theorems · Definition · general topology

Profinite.of

(X : Type u_1) → [inst : TopologicalSpace X] → [CompactSpace X] → [T2Space X] → [TotallyDisconnectedSpace X] → Profinite

Construct a term of Profinite from a type endowed with the structure of a compact, Hausdorff and totally disconnected topological space.

Defined in

Mathlib.Topology.Category.Profinite.Basic

Cited by

11 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

TopologicalSpaceCompactSpaceT2SpaceTotallyDisconnectedSpace