Theorem MeasureTheory.SigmaFinite.of_trim

Modification history

2026-03-06 15:35
Mathlib/MeasureTheory/Measure/Trim.lean
feat: Radon-Nikodym derivative of a map is a conditional expectation (#35089) …
Added MeasureTheory.SigmaFinite.of_trimView on Github →