Stone-Čech compactification #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Construction of the Stone-Čech compactification using ultrafilters.
Parts of the formalization are based on "Ultrafilters and Topology"
by Marius Stekelenburg, particularly section 5.
The basic open sets for the topology on ultrafilters are open.
The basic open sets for the topology on ultrafilters are also closed.
pure : α → ultra_filter α induces on
α the discrete topology.
The extension of a function
α → γ to a function
ultrafilter α → γ.
γ is a compact Hausdorff space it will be continuous.
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.
The natural map from α to its Stone-Čech compactification.
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 α.