Commit 2023-12-01 14:20 42649c4d

View on Github →

chore: use StandardBorelSpace instead of PolishSpace in the Probability folder (#8762) Also replace some Type _ with Type*.

Estimated changes

Modified Mathlib/Probability/Independence/Conditional.lean

modified theorem ProbabilityTheory.CondIndep.symm

modified theorem ProbabilityTheory.CondIndepFun.comp

modified def ProbabilityTheory.CondIndepFun

modified theorem ProbabilityTheory.condIndepFun_iff

modified theorem ProbabilityTheory.condIndepFun_iff_condIndep

modified theorem ProbabilityTheory.condIndep_iff_condIndepSets

modified theorem ProbabilityTheory.iCondIndepFun.condIndepFun

modified theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset

modified theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prod

modified def ProbabilityTheory.iCondIndepFun

modified theorem ProbabilityTheory.iCondIndepFun_iff

modified theorem ProbabilityTheory.iCondIndepFun_iff_condexp_inter_preimage_eq_mul

modified theorem ProbabilityTheory.iCondIndepFun_iff_iCondIndep

Modified Mathlib/Probability/Independence/ZeroOne.lean

modified theorem ProbabilityTheory.condIndep_biSup_compl

modified theorem ProbabilityTheory.condIndep_biSup_limsup

modified theorem ProbabilityTheory.condIndep_iSup_directed_limsup

modified theorem ProbabilityTheory.condIndep_iSup_limsup

modified theorem ProbabilityTheory.condIndep_limsup_atBot_self

modified theorem ProbabilityTheory.condIndep_limsup_atTop_self

modified theorem ProbabilityTheory.condIndep_limsup_self

modified theorem ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup

modified theorem ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup_atBot

modified theorem ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup_atTop