Commit 2024-01-31 15:04 040db1bb

View on Github →

refactor(Probability/Kernel/CondCdf): mv lintegral_iInf_directed_of_measurable (#10041)

depends on: #10036

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

added theorem MeasureTheory.lintegral_iInf_directed_of_measurable

Modified Mathlib/Probability/Kernel/CondCdf.lean

deleted theorem lintegral_iInf_directed_of_measurable