mathlib

001ffdc4 - feat(probability/independence): Independence of singletons (#18506)

feat(probability/independence): Independence of singletons (#18506) Characterisation of independence in terms of measure distributing over finite intersections, and lemmas connecting the different concepts of independence. Also add supporting `measurable_space` and `set.preimage` lemmas