Commit 2023-07-11 20:21 f61c1f29

View on Github →

feat: add SeparableSpace instances (#5801)

Estimated changes

Modified Mathlib/Data/Set/Countable.lean

added theorem Set.countable_univ_iff

Modified Mathlib/Topology/Bases.lean

added theorem QuotientMap.separableSpace

added theorem TopologicalSpace.SeparableSpace.of_denseRange

added theorem TopologicalSpace.separableSpace_iff_countable

deleted theorem TopologicalSpace.separableSpace_of_denseRange