Commit 2025-03-06 09:48 55784a74

View on Github →

feat(ProbabilityTheory/Independence/Basic): Upstream independence lemmas from PFR (#22516) These lemmas are from the PFR Project.

Estimated changes

Modified Mathlib/Probability/Independence/Basic.lean

added theorem ProbabilityTheory.iIndep.of_subsingleton

added theorem ProbabilityTheory.iIndepFun.of_precomp

modified theorem ProbabilityTheory.iIndepFun.of_subsingleton

added theorem ProbabilityTheory.iIndepFun.precomp

added theorem ProbabilityTheory.iIndepFun_precomp_of_bijective

added theorem ProbabilityTheory.iIndepSets.of_subsingleton

Modified Mathlib/Probability/Independence/Kernel.lean

added theorem ProbabilityTheory.Kernel.iIndep.of_subsingleton

modified theorem ProbabilityTheory.Kernel.iIndepFun.of_subsingleton

added theorem ProbabilityTheory.Kernel.iIndepSets.of_subsingleton