mathlib3

d1bb5ea6 - feat(topology/category/Compactum): Compact Hausdorff spaces (#4555)

feat(topology/category/Compactum): Compact Hausdorff spaces (#4555) This PR provides the equivalence between the category of compact Hausdorff topological spaces and the category of algebras for the ultrafilter monad. ## Notation 1. `Compactum` is the category of algebras for the ultrafilter monad. It's a wrapper around `monad.algebra (of_type_functor $ ultrafilter)`. 2. `CompHaus` is the full subcategory of `Top` consisting of topological spaces which are compact and Hausdorff.