PR #9387: feat(probability_theory/independence): if a fam...

Stream: triage

[Random Issue Bot]

Today I chose PR 9387 for discussion!

feat(probability_theory/independence): if a family of pi-systems is independent, then so are the generated measurable spaces
Created by @Rémy Degenne (@RemyDegenne) on 2021-09-25
Labels: WIP

Is this PR still relevant? Any recent updates? Anyone making progress?