Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-23 00:02 316d69fe

View on Github →

feat(measure_theory/measure_space): add measurable set lemma for symmetric differences (#8401)

Estimated changes

Modified src/measure_theory/measurable_space_def.lean

added theorem measurable_set.cond

added theorem measurable_set.symm_diff

Modified src/measure_theory/measure_space.lean

deleted theorem measurable_set.cond

Modified src/measure_theory/tactic.lean