Def MeasureTheory.Filtration.piFinset

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.piFinsetView on Github →