Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-18 12:22 496a744e

View on Github →

feat(measure_theory): generalize null_of_locally_null to outer_measure, add versions (#11535)

generalize null_of_locally_null;
don't intersect with s twice;
add a contraposed version;
golf.

Estimated changes

Modified src/measure_theory/covering/differentiation.lean

Modified src/measure_theory/covering/vitali.lean

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.exists_mem_forall_mem_nhds_within_pos_measure

added theorem measure_theory.exists_ne_forall_mem_nhds_pos_measure_preimage

modified theorem measure_theory.null_of_locally_null

Modified src/measure_theory/measure/outer_measure.lean

added theorem measure_theory.outer_measure.exists_mem_forall_mem_nhds_within_pos

added theorem measure_theory.outer_measure.null_of_locally_null

Modified src/topology/metric_space/basic.lean

added theorem metric.diam_le_of_subset_closed_ball