mathlib

3164b1ad - feat(probability/independence): two lemmas on indep_fun (#13126)

feat(probability/independence): two lemmas on indep_fun (#13126) These two lemmas show that `indep_fun` is preserved under composition by measurable maps and under a.e. equality.