Theorem MeasurableSet.induction_on_open

Modification history

2024-12-14 15:50
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
chore: make some `induction_on*` compatible with `induction` (#19898)
Modified MeasurableSet.induction_on_openView on Github →
2023-05-21 12:07
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
feat: port MeasureTheory.Constructions.BorelSpace.Basic (#4018)
Added MeasurableSet.induction_on_openView on Github →