Theorem ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_map_map

Modification history

2025-10-01 13:25
Mathlib/Probability/Independence/Conditional.lean
feat(Probability/Independence): relate conditional independence and factorization of a kernel (#29884) …
Added ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_map_mapView on Github →