Commit 2025-04-10 07:25 b759d204

View on Github →

feat: any function from a countable discrete domain is strongly measurable (#23862) Also deprecate StronglyMeasurable.of_finite, which has become a corollary, and rename Subsingleton.stronglyMeasurable/Subsingleton.stronglyMeasurable' to StronglyMeasurable.of_subsingleton_cod/StronglyMeasurable.of_subsingleton_dom for clarity. From LeanAPAP

Estimated changes

Modified Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean

added theorem MeasureTheory.AEStronglyMeasurable.of_discrete

modified theorem MeasureTheory.AEStronglyMeasurable.of_finite

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

added theorem MeasureTheory.StronglyMeasurable.of_discrete

modified theorem MeasureTheory.StronglyMeasurable.of_finite

added theorem MeasureTheory.StronglyMeasurable.of_subsingleton_cod

added theorem MeasureTheory.StronglyMeasurable.of_subsingleton_dom

modified theorem MeasureTheory.Subsingleton.stronglyMeasurable'

modified theorem MeasureTheory.Subsingleton.stronglyMeasurable