mathlib

dabb0c61 - feat(probability/independence): equivalent ways to check indep_fun (#14814)

feat(probability/independence): equivalent ways to check indep_fun (#14814) Prove: - `indep_fun f g μ ↔ ∀ s t, measurable_set s → measurable_set t → μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)`, - `indep_fun f g μ ↔ ∀ s t, measurable_set s → measurable_set t → indep_set (f ⁻¹' s) (g ⁻¹' t) μ`.