Commit 2022-01-31 15:42 c04daaf4

View on Github →

feat(measure_theory): typeclass for measures positive on nonempty opens (#11652) Add a typeclass for measures positive on nonempty opens, migrate is(_add?)_haar_measure to this API.

Estimated changes

Modified src/measure_theory/constructions/borel_space.lean

added theorem continuous.is_open_pos_measure_map

Modified src/measure_theory/covering/besicovitch_vector_space.lean

Modified src/measure_theory/group/basic.lean

deleted theorem is_open.haar_pos

added theorem measure_theory.is_open_pos_measure_of_mul_left_invariant_of_compact

added theorem measure_theory.is_open_pos_measure_of_mul_left_invariant_of_regular

deleted theorem measure_theory.measure.haar_pos_of_nonempty_interior

deleted theorem measure_theory.measure_pos_of_is_open_of_is_mul_left_invariant

deleted theorem measure_theory.null_iff_empty_of_is_mul_left_invariant

Modified src/measure_theory/integral/interval_integral.lean

Modified src/measure_theory/measure/haar.lean

Modified src/measure_theory/measure/haar_lebesgue.lean

deleted theorem measure_theory.measure.add_haar_ball_pos

deleted theorem measure_theory.measure.add_haar_closed_ball_pos

Created src/measure_theory/measure/open_pos.lean

added theorem continuous.ae_eq_iff_eq

added theorem emetric.measure_ball_pos

added theorem emetric.measure_closed_ball_pos

added theorem has_le.le.is_open_pos_measure

added theorem is_open.eq_empty_of_measure_zero

added theorem is_open.measure_eq_zero_iff

added theorem is_open.measure_ne_zero

added theorem is_open.measure_pos

added theorem is_open.measure_pos_iff

added theorem measure_theory.measure.eq_of_ae_eq

added theorem measure_theory.measure.eq_on_Icc_of_ae_eq

added theorem measure_theory.measure.eq_on_Ico_of_ae_eq

added theorem measure_theory.measure.eq_on_Ioc_of_ae_eq

added theorem measure_theory.measure.eq_on_Ioo_of_ae_eq

added theorem measure_theory.measure.eq_on_of_ae_eq

added theorem measure_theory.measure.eq_on_open_of_ae_eq

added theorem measure_theory.measure.interior_eq_empty_of_null

added theorem measure_theory.measure.is_open_pos_measure_smul

added theorem measure_theory.measure.measure_Iio_pos

added theorem measure_theory.measure.measure_Ioi_pos

added theorem measure_theory.measure.measure_Ioo_eq_zero

added theorem measure_theory.measure.measure_Ioo_pos

added theorem measure_theory.measure.measure_pos_of_mem_nhds

added theorem measure_theory.measure.measure_pos_of_nonempty_interior

added theorem metric.measure_ball_pos

added theorem metric.measure_closed_ball_pos

Modified src/topology/algebra/ordered/basic.lean

added theorem Ico_subset_closure_interior

added theorem Ioc_subset_closure_interior

added theorem Ioo_subset_closure_interior

added theorem closure_interior_Icc

Modified src/topology/separation.lean

added theorem set.eq_on.of_subset_closure