Commit 2026-10-02 17:43 19cdde90

View on Github →

chore: rename sFinite to sfinite in declaration names (#44292) Rename the declarations spelling the SFinite class as sFinite to use sfinite, following the rule that the whole initial run of capitals is lowercased.

Estimated changes

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

Modified Mathlib/MeasureTheory/Function/ConditionalLExpectation.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/DistLEIntegral.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Countable.lean

Modified Mathlib/MeasureTheory/Measure/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean

deleted theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite

added theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sfinite

deleted theorem MeasureTheory.Measure.restrict_toMeasurable_of_sFinite

added theorem MeasureTheory.Measure.restrict_toMeasurable_of_sfinite

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

deleted theorem MeasureTheory.sFinite_of_absolutelyContinuous

added theorem MeasureTheory.sfinite_of_absolutelyContinuous

Modified Mathlib/Probability/Kernel/Basic.lean

Modified Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean

Modified Mathlib/Probability/Kernel/Defs.lean