Theorems · Definition · general topology

LightProfinite.of

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

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

Defined in

Mathlib.Topology.Category.LightProfinite.Basic

Cited by

19 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

TopologicalSpaceCompactSpaceT2SpaceTotallyDisconnectedSpaceSecondCountableTopology