Theorem ProbabilityTheory.set_integral_stieltjesOfMeasurableRat_rat

Modification history

2024-04-18 02:39

Mathlib/Probability/Kernel/Disintegration/CdfToKernel.lean

chore: replace `set_integral` with `setIntegral` (#12215) …

Deleted ProbabilityTheory.set_integral_stieltjesOfMeasurableRat_rat View on Github →

2024-03-17 17:51

Mathlib/Probability/Kernel/Disintegration/CdfToKernel.lean

feat(Probability/Kernel): build a kernel from a kernel CDF (#11209) …

Added ProbabilityTheory.set_integral_stieltjesOfMeasurableRat_rat View on Github →