Theorem ProbabilityTheory.isRatCondKernelCDFAux.tendsto_one_of_monotone

Modification history

2024-03-27 14:40

Mathlib/Probability/Kernel/Disintegration/CdfToKernel.lean

refactor: use CdfToKernel in CondCdf (#11529) …

Deleted ProbabilityTheory.isRatCondKernelCDFAux.tendsto_one_of_monotone 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.isRatCondKernelCDFAux.tendsto_one_of_monotone View on Github →