Commit 2024-06-15 21:09 0ac1ced0

View on Github →

feat: weaken 2nd countable to lindelof in Regular+Lindelof=>Normal (#13176)

Estimated changes

Modified Mathlib/Topology/Basic.lean

added theorem closure_iUnion₂_le_nat

added theorem closure_iUnion₂_lt_nat

added theorem interior_iInter₂_le_nat

added theorem interior_iInter₂_lt_nat

Modified Mathlib/Topology/Compactness/Lindelof.lean

added theorem IsLindelof.indexed_countable_subcover

Modified Mathlib/Topology/Separation.lean

added def HasSeparatingCover

added theorem IsClosed.HasSeparatingCover

added theorem hasSeparatingCovers_iff_separatedNhds

Modified docs/references.bib