Theorem MeasureTheory.StronglyMeasurable.dependsOn_of_piFinset

Modification history

2025-03-06 11:53
Mathlib/MeasureTheory/Function/FactorsThrough.lean
feat: filtration of events which only depends on a finite number of coordinates (#22584) …
Added MeasureTheory.StronglyMeasurable.dependsOn_of_piFinsetView on Github →