Commit 2021-03-14 00:42 f4c4d107

feat(probability_theory/independence): prove equivalences for indep_set (#6242) Prove the following equivalences on indep_set, for measurable sets s,t and a probability measure µ :

• indep_set s t μ ↔ μ (s ∩ t) = μ s * μ t,
• indep_set s t μ ↔ indep_sets {s} {t} μ. In indep_sets.indep_set_of_mem, we use those equivalences to obtain indep_set s t µ from indep_sets S T µ and s ∈ S, t ∈ T.