2021-07-18 17:02
src/measure_theory/measure_space.lean
feat(measure_theory): add lemmas of equality of measures under assumptions of null difference, in particular null frontier (#8332) …
Added measure_theory.meas_eq_meas_smaller_of_between_null_diff