1.12. ForMathlib.Probability.Independence.IndepInfinitePi🔗

Lemmas about independence and infinite products

Module LeanMachineLearning.ForMathlib.Probability.Independence.IndepInfinitePi contains 2 exposed declarations.

• MeasurableSpace.comap_piLemma · 0 deps
• ProbabilityTheory.indepFun_proj_infinitePi_infinitePiLemma · 0 deps