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_uncurryView on Github →