mathlib3
0bd6dc2a - chore(measure_theory): move and rename some lemmas (#12699)

Commit
3 years ago
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.
Author
Parents
Loading