feat(Probability/Independence): grouping an independent family by pairwise disjoint index sets#41935

martinamaggio wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

martinamaggio:MM/iIndep_iSup_of_disjointmartinamaggio/mathlib4:MM/iIndep_iSup_of_disjointCopy head branch name to clipboard