Commit 2023-11-30 18:08 6aa29281

View on Github →

chore: use StandardBorelSpace everywhere in the probability folder instead of PolishSpace (#8746)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Polish.lean

Modified Mathlib/Probability/Kernel/CondDistrib.lean

Modified Mathlib/Probability/Kernel/Condexp.lean

modified theorem ProbabilityTheory.condexpKernel_apply_eq_condDistrib

Modified Mathlib/Probability/Kernel/Disintegration.lean