Theorem ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry

Modification history

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