mathlib3

78a518a3 - feat(measure_theory/independence): define independence of sets of sets, measurable spaces, sets, functions (#5848)

feat(measure_theory/independence): define independence of sets of sets, measurable spaces, sets, functions (#5848) This first PR about independence contains definitions, a few lemmas about independence of unions/intersections of sets of sets, and a proof that two measurable spaces are independent iff generating pi-systems are independent (included in this PR to demonstrate usability of the definitions). Co-authored-by: Rémy Degenne <remydegenne@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>