Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-14 04:32 8dffafd2

View on Github →

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

Estimated changes

added theorem set.maps_to_singleton
added theorem filter.has_basis_pure
modified theorem filter.tendsto_comap_iff
modified theorem filter.tendsto_map'_iff
modified theorem filter.tendsto_sup
added theorem ultrafilter.coe_comap
added theorem ultrafilter.mem_comap
added theorem alexandroff.coe_eq_coe
added def alexandroff
added theorem is_open.nhds_within_eq
deleted theorem nhds_within_eq_of_open
modified def filter.cocompact
modified theorem filter.has_basis_cocompact
modified theorem filter.mem_cocompact'
modified theorem filter.mem_cocompact
added theorem is_compact_univ_iff