Theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sfinite

Modification history

2026-10-02 17:43
Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean
chore: rename `sFinite` to `sfinite` in declaration names (#44292) …
Added MeasureTheory.Measure.measure_toMeasurable_inter_of_sfiniteView on Github →