1.23. ForMathlib.Probability.Independence.IndepInfinitePi🔗

Lemmas about independence and infinite products

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

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