Theorem ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map

Modification history

2025-08-03 18:35
Mathlib/Probability/Independence/InfinitePi.lean
feat: random variables are independent iff their joint distribution is the product measure (#26265) …
Added ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_mapView on Github →