Commit 2024-11-14 11:04 16303ca7

View on Github →

feat: generalize tendsto_measure_iInter (#18540)

Estimated changes

Modified Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean

Modified Mathlib/MeasureTheory/Function/Egorov.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem Antitone.measure_iInter

added theorem Directed.measure_iInter

deleted theorem MeasureTheory.measure_iInter_eq_iInf'

deleted theorem MeasureTheory.measure_iInter_eq_iInf

added theorem MeasureTheory.measure_iInter_eq_iInf_measure_iInter_le

deleted theorem MeasureTheory.tendsto_measure_iInter'

deleted theorem MeasureTheory.tendsto_measure_iInter

added theorem MeasureTheory.tendsto_measure_iInter_atBot

added theorem MeasureTheory.tendsto_measure_iInter_atTop

added theorem MeasureTheory.tendsto_measure_iInter_le

added theorem Monotone.measure_iInter

Modified Mathlib/MeasureTheory/Measure/NullMeasurable.lean

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

Modified Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean

Modified Mathlib/Probability/Kernel/Disintegration/CondCDF.lean

Modified Mathlib/Probability/Kernel/Disintegration/Density.lean