mathlib

13486fe5 - chore(measure_theory/measure_space): untangle `probability_measure`, `finite_measure`, and `has_no_atoms` (#8222)

chore(measure_theory/measure_space): untangle `probability_measure`, `finite_measure`, and `has_no_atoms` (#8222) This only moves existing lemmas around. Putting all the instance together up front seems to result in lemmas being added in adhoc places - by adding `section`s, this should guide future contributions.