Commit 2022-01-06 07:05 b3260f37

feat(measure_theory/constructions/borel_space): new lemma tendsto_measure_cthickening (#11009) Prove that, when r tends to 0, the measure of the r-thickening of a set s tends to the measure of s.