Theorem MeasureTheory.Filtration.piFinset_eq_comap_restrict

Modification history

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