Theorem MeasureTheory.integral_of_not_completeSpace

Modification history

2026-06-03 07:58
Mathlib/MeasureTheory/Integral/Bochner/Basic.lean
feat: missing small lemmas in measure theory, cleanup (#40106)
Added MeasureTheory.integral_of_not_completeSpaceView on Github →