Commit 2025-06-22 22:27 dfe27eb2

View on Github →

style: rename EventuallyMeasurableSpace to eventuallyMeasurableSpace (#26232) EventuallyMeasurableSpace isn't a type name, so should be renamed to eventuallyMeasurableSpace.

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/EventuallyMeasurable.lean

modified def EventuallyMeasurable

deleted theorem EventuallyMeasurableSpace.measurable_le

deleted def EventuallyMeasurableSpace

added def eventuallyMeasurableSpace

added theorem le_eventuallyMeasurableSpace

Modified Mathlib/MeasureTheory/Measure/NullMeasurable.lean

Modified Mathlib/Topology/Baire/BaireMeasurable.lean