Mathlib Changelog
v4
Changelog
About
Github
Theorem
MeasureTheory.StronglyMeasurable.of_subsingleton_dom
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_subsingleton_dom
View on Github →