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.
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 extension of a continuous function from α to a compact Hausdorff space γ to the Stone-Čech compactification of α.