Commit 2021-01-27 12:14 78a518a3

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).