mathlib3

b3260f37 - feat(measure_theory/constructions/borel_space): new lemma tendsto_measure_cthickening (#11009)

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`.