Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-17 07:20 43bbaee8

View on Github →

feat(measure_theory/measure): add lemmas, drop measurable_set assumptions (#11499)

  • restrict_eq_self no longer requires measurability of either set;
  • restrict_apply_self no longer requires measurability of the set;
  • add restrict_apply_superset and restrict_restrict_of_subset ;
  • add restrict_restrict' that assumes measurability of the other set, drop one measurable_set assumption in restrict_comm;
  • drop measurability assumptions in restrict_congr_mono.

Estimated changes