Commit 2024-09-18 11:42 f85eaad5

View on Github →

feat(MeasureTheory): generalize measure_iUnion_eq_iSup (#16390)

Estimated changes

Modified Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem Antitone.measure_iUnion

added theorem Directed.measure_iUnion

modified theorem MeasureTheory.measure_iUnion_congr_of_subset

deleted theorem MeasureTheory.measure_iUnion_eq_iSup'

deleted theorem MeasureTheory.measure_iUnion_eq_iSup

added theorem MeasureTheory.measure_iUnion_eq_iSup_accumulate

modified theorem MeasureTheory.measure_iUnion_toMeasurable

modified theorem MeasureTheory.tendsto_measure_Ici_atBot

modified theorem MeasureTheory.tendsto_measure_Ico_atTop

modified theorem MeasureTheory.tendsto_measure_Iic_atTop

modified theorem MeasureTheory.tendsto_measure_Ioc_atBot

deleted theorem MeasureTheory.tendsto_measure_iUnion'

deleted theorem MeasureTheory.tendsto_measure_iUnion

added theorem MeasureTheory.tendsto_measure_iUnion_accumulate

added theorem MeasureTheory.tendsto_measure_iUnion_atBot

added theorem MeasureTheory.tendsto_measure_iUnion_atTop

added theorem Monotone.measure_iUnion

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

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

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

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

Modified Mathlib/Probability/StrongLaw.lean