Theorem MeasureTheory.StronglyMeasurable.exists_eq_measurable_comp

Modification history

2025-03-24 16:18
Mathlib/MeasureTheory/Function/FactorsThrough.lean
feat: if `g` is measurable wrt to the pullback by `f` then `g` is a measurable function of `f` (#22743) …
Added MeasureTheory.StronglyMeasurable.exists_eq_measurable_compView on Github →