Theorem aemeasurable_pi_iff

Modification history

2025-03-29 13:22
Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
feat(Probability/Independence/Basic): upstream `iIndepFun_iff_pi_map_eq_map` from PFR (#23418) …
Added aemeasurable_pi_iffView on Github →