Theorem measurableSet_insert

Modification history

2024-08-03 10:01

Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

chore: remove some uses of `open Classical`, part 2 (#15413) …

Modified measurableSet_insert View on Github →

2023-02-06 20:02

Mathlib/MeasureTheory/MeasurableSpaceDef.lean

feat: port MeasureTheory.MeasurableSpaceDef (#2108)

Added measurableSet_insert View on Github →