Commit 2025-11-24 14:10 c398cab9

View on Github →

feat(Probability/Independence): reindexing lemmas for iIndep* (#31309)

Estimated changes

Modified Mathlib/Probability/Independence/Basic.lean

added theorem ProbabilityTheory.iIndep.of_precomp

added theorem ProbabilityTheory.iIndep.precomp

modified theorem ProbabilityTheory.iIndepFun.of_precomp

modified theorem ProbabilityTheory.iIndepFun.precomp

modified theorem ProbabilityTheory.iIndepFun_precomp_of_bijective

added theorem ProbabilityTheory.iIndepSet.of_precomp

added theorem ProbabilityTheory.iIndepSet.precomp

added theorem ProbabilityTheory.iIndepSet_precomp_of_bijective

added theorem ProbabilityTheory.iIndepSets.of_precomp

added theorem ProbabilityTheory.iIndepSets.precomp

added theorem ProbabilityTheory.iIndepSets_precomp_of_bijective

added theorem ProbabilityTheory.iIndep_precomp_of_bijective

Modified Mathlib/Probability/Independence/Kernel.lean

added theorem ProbabilityTheory.Kernel.iIndep.of_precomp

added theorem ProbabilityTheory.Kernel.iIndep.precomp

added theorem ProbabilityTheory.Kernel.iIndepFun.of_precomp

added theorem ProbabilityTheory.Kernel.iIndepFun.precomp

added theorem ProbabilityTheory.Kernel.iIndepFun_precomp_of_bijective

added theorem ProbabilityTheory.Kernel.iIndepSet.of_precomp

added theorem ProbabilityTheory.Kernel.iIndepSet.precomp

added theorem ProbabilityTheory.Kernel.iIndepSet_precomp_of_bijective

added theorem ProbabilityTheory.Kernel.iIndepSets.of_precomp

added theorem ProbabilityTheory.Kernel.iIndepSets.precomp

added theorem ProbabilityTheory.Kernel.iIndepSets_precomp_of_bijective

added theorem ProbabilityTheory.Kernel.iIndep_precomp_of_bijective