Mathlib Changelog
v4
Changelog
About
Github
Theorem
ContinuousMapZero.aeStronglyMeasurable_mkD_restrict_of_uncurry
Modification history
2025-06-21 12:16
Mathlib/MeasureTheory/SpecificCodomains/ContinuousMapZero.lean
feat: specific lemmas about integrability of ContinuousMap[Zero]-valued functions (#26058) …
Added
ContinuousMapZero.aeStronglyMeasurable_mkD_restrict_of_uncurry
View on Github →