Theorem discreteTopology_of_noAccPts

Modification history

2026-01-29 13:31

Mathlib/Topology/DiscreteSubset.lean

feat(MeasureTheory/Measure/TypeClass/NoAtoms): add `exists_accPt_of_noAtoms` (#32851) …

Added discreteTopology_of_noAccPts View on Github →