Commit 2025-03-06 11:53 9d606847

feat: filtration of events which only depends on a finite number of coordinates (#22584) Introduce a filtration on the product space Π i, X i: piFinset s is the set of events which only depend on coordinates in s. Prove that if a function is measurable with respect to piFinset s then it only depends on coordinates in s.