Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-15 08:11 0bd6dc2a

View on Github →

chore(measure_theory): move and rename some lemmas (#12699)

  • move ae_interval_oc_iff, ae_measurable_interval_oc_iff, and ae_interval_oc_iff' to measure_theory.measure.measure_space, rename ae_interval_oc_iff' to ae_restrict_interval_oc_iff;
  • add lemmas about ae and union of sets.

Estimated changes

deleted theorem ae_interval_oc_iff'
deleted theorem ae_interval_oc_iff