Commit 2026-01-29 13:31 dfa111ce

feat(MeasureTheory/Measure/TypeClass/NoAtoms): add exists_accPt_of_noAtoms (#32851) feat(MeasureTheory/Measure/TypeClass/NoAtoms): Added a theorem that states If a set has positive measure under an atomless measure, then it has an accumulation point. Added a lemma in (Topology/DiscreteSubset): If a subset of a topological space has no accumulation points, then it carries the discrete topology. Theorem added: exists_accPt_of_pos_hausdorffMeasure Lemma added: discreteTopology_of_noAccPts Harmonic's Aristotle gave the initial version of the proofs. I did substantial work shortening the proof from 40 lines and refactoring it into another Lemma. Special thanks to @plp127 and @CoolRmal for the useful feedback in the PR process.