Theorem MeasureTheory.Measure.IicSnd_le_fst

Modification history

2024-09-01 12:32
Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
chore(Measure): add `gcongr` lemmas (#16379)
Modified MeasureTheory.Measure.IicSnd_le_fstView on Github →
2024-03-27 14:40
Mathlib/Probability/Kernel/CondCdf.lean
refactor: use CdfToKernel in CondCdf (#11529) …
Modified MeasureTheory.Measure.IicSnd_le_fstView on Github →
2023-06-16 15:28
Mathlib/Probability/Kernel/CondCdf.lean
feat: port Probability.Kernel.CondCdf (#5143)
Added MeasureTheory.Measure.IicSnd_le_fstView on Github →