mathlib

8dffafd2 - feat(topology): one-point compactification of a topological space (#8579)

feat(topology): one-point compactification of a topological space (#8579) Define `alexandroff X` to be the one-point compactification of a topological space `X` and prove some basic lemmas about this definition. Co-authored by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Yourong "DZR" Zang <yourongzang@outlook.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>