Theorem MeasurableSpace.measurableSet_inf

Modification history

2025-03-31 05:22

Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

refactor(MeasureTheory): fix `simp` not applying `measurableSet_inf` (#23270) …

Modified MeasurableSpace.measurableSet_inf View on Github →

2023-02-06 20:02

Mathlib/MeasureTheory/MeasurableSpaceDef.lean

feat: port MeasureTheory.MeasurableSpaceDef (#2108)

Added MeasurableSpace.measurableSet_inf View on Github →