Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-23 13:55 59ef8ce5

View on Github →

feat(measure_theory/measure): assorted lemmas (#11612)

  • add ae_disjoint_compl_left/right;
  • deduce restrict_to_measurable and restrict_to_measurable_of_sigma_finite from @sgouezel 's lemmas about measures of intersections;
  • add ae_restrict_mem₀;
  • add ae_eq_univ.

Estimated changes