Theorem EventuallyMeasurableSpace.measurable_le

Modification history

2025-06-22 22:27

Mathlib/MeasureTheory/MeasurableSpace/EventuallyMeasurable.lean

style: rename `EventuallyMeasurableSpace` to `eventuallyMeasurableSpace` (#26232) …

Deleted EventuallyMeasurableSpace.measurable_le View on Github →

2024-06-08 17:32

Mathlib/MeasureTheory/Constructions/EventuallyMeasurable.lean

feat(MeasureTheory): generalize NullMeasurable to measurability mod a sigma filter. (#10856) …

Added EventuallyMeasurableSpace.measurable_le View on Github →