2025-06-21 12:16
Mathlib/MeasureTheory/SpecificCodomains/ContinuousMapZero.lean
feat: specific lemmas about integrability of ContinuousMap[Zero]-valued functions (#26058) …
Added ContinuousMapZero.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry