Theorem ContinuousMapZero.hasFiniteIntegral_mkD_restrict_of_bound

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.hasFiniteIntegral_mkD_restrict_of_boundView on Github →