Commit 2021-07-18 17:02 b02b9197

feat(measure_theory): add lemmas of equality of measures under assumptions of null difference, in particular null frontier (#8332) Adding lemmas in measure_theory/measure_space and measure_theory/borel_space about equality of measures of sets under the assumption that the difference of the largest to the smallest has null measure.