Theorem ProbabilityTheory.condIndepFun_of_measurable_right

Modification history

2025-09-26 12:24
Mathlib/Probability/Independence/Conditional.lean
feat(Probability): `CondIndepFun` lemmas (#29554) …
Added ProbabilityTheory.condIndepFun_of_measurable_rightView on Github →