mathlib3
dbf038d6 - feat(topology/category): constructor for compact hausdorff spaces (#6068)

Commit

4 years ago

feat(topology/category): constructor for compact hausdorff spaces (#6068) `CompHaus.of` constructor. From the lean-liquid project.

Author

b-mehta

Parents