Stone-Čech compactification #
Construction of the Stone-Čech compactification using ultrafilters.
Parts of the formalization are based on "Ultrafilters and Topology" by Marius Stekelenburg, particularly section 5.
Basis for the topology on Ultrafilter α
.
Instances For
Every ultrafilter u
on Ultrafilter α
converges to a unique
point of Ultrafilter α
, namely joinM u
.
The range of pure : α → Ultrafilter α
is dense in Ultrafilter α
.
The map pure : α → Ultrafilter α
induces on α
the discrete topology.
pure : α → Ultrafilter α
defines a dense inducing of α
in Ultrafilter α
.
pure : α → Ultrafilter α
defines a dense embedding of α
in Ultrafilter α
.
The extension of a function α → γ
to a function Ultrafilter α → γ
.
When γ
is a compact Hausdorff space it will be continuous.
Instances For
The value of Ultrafilter.extend f
on an ultrafilter b
is the
unique limit of the ultrafilter b.map f
in γ
.
The Stone-Čech compactification of a topological space.
Instances For
The natural map from α to its Stone-Čech compactification.
Instances For
The image of stone_cech_unit is dense. (But stone_cech_unit need not be an embedding, for example if α is not Hausdorff.)
The extension of a continuous function from α to a compact Hausdorff space γ to the Stone-Čech compactification of α.