English
There is a canonical way to form a LightProfinite from aType X equipped with compact, Hausdorff, totally disconnected and second countable topology; i.e., given X with these structures, LightProfinite.of X is an object in LightProfinite.
Русский
Существуют условия для перехода типа X с компактной, гомеоморфной к Hausdorff, полной разобщённостью и вторым счётом к топологии LightProfinite; т.е. LightProfinite.of X — это объект в LightProfinite.
LaTeX
$$$\text{LightProfinite.of}: (X, \text{top}) \mapsto \text{LightProfinite}$$$
Lean4
/-- Construct a term of `LightProfinite` from a type endowed with the structure of a compact,
Hausdorff, totally disconnected and second countable topological space.
-/
abbrev of (X : Type*) [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X]
[SecondCountableTopology X] : LightProfinite :=
CompHausLike.of _ X
