English
A Stonean space is constructed from a type X equipped with a topology, compactness, T2 (Hausdorff), and extremal disconnectedness by taking Stonean to be CompHausLike.of X.
Русский
Пусть X — множество с топологией, компактное, T2 (Хаусдорфово) и экстремально разобщенное; тогда образ Stonean(X) задается как CompHausLike.of X.
LaTeX
$$$\text{Stonean}(X) = \text{CompHausLike.of}(X)$$$
Lean4
/-- Construct a term of `Stonean` from a type endowed with the structure of a
compact, Hausdorff and extremally disconnected topological space.
-/
abbrev of (X : Type*) [TopologicalSpace X] [CompactSpace X] [T2Space X] [ExtremallyDisconnected X] : Stonean :=
CompHausLike.of _ X
