Def EventuallyMeasurableSpace

Modification history

2025-06-22 22:27
Mathlib/MeasureTheory/MeasurableSpace/EventuallyMeasurable.lean
style: rename `EventuallyMeasurableSpace` to `eventuallyMeasurableSpace` (#26232) …
Deleted EventuallyMeasurableSpaceView on Github →
2024-08-19 11:42
Mathlib/MeasureTheory/Constructions/EventuallyMeasurable.lean
chore: backports from byAsSorry (#15759) …
Modified EventuallyMeasurableSpaceView on Github →
2024-06-08 17:32
Mathlib/MeasureTheory/Constructions/EventuallyMeasurable.lean
feat(MeasureTheory): generalize NullMeasurable to measurability mod a sigma filter. (#10856) …
Added EventuallyMeasurableSpaceView on Github →