Theorem MeasureTheory.AEStronglyMeasurable.of_discrete

Modification history

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