Theorem MeasureTheory.FiniteMeasure.measurableSet_isFiniteMeasure

Modification history

2025-03-06 11:11
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
feat: Giry monoidal product (#22062) …
Added MeasureTheory.FiniteMeasure.measurableSet_isFiniteMeasureView on Github →