Theorem MeasureTheory.StronglyMeasurable.of_discrete

Modification history

2025-04-10 07:25
Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
feat: any function from a countable discrete domain is strongly measurable (#23862) …
Added MeasureTheory.StronglyMeasurable.of_discreteView on Github →