Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-22 01:15 c4c71d2f

View on Github →

feat(topology): define class [noncompact_space] (#9839)

Estimated changes

Modified src/topology/alexandroff.lean

modified theorem alexandroff.dense_embedding_coe

modified theorem alexandroff.dense_range_coe

Modified src/topology/instances/real.lean

Modified src/topology/metric_space/basic.lean

added theorem metric.diam_univ_of_noncompact

added theorem metric.ediam_univ_eq_top_iff_noncompact

added theorem metric.ediam_univ_of_noncompact

Modified src/topology/subset_properties.lean

added theorem filter.cocompact_ne_bot_iff

deleted theorem filter.cocompact_ne_bot_tfae

modified theorem filter.coprod_cocompact

added theorem noncompact_space_of_ne_bot

added theorem not_compact_space_iff

added theorem prod.noncompact_space_iff