Commit 2024-11-05 19:27 0d3f34a5

View on Github →

feat(SetIntegral): generalize tendsto_setIntegral_of_monotone (#18639)

Estimated changes

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

modified theorem MeasureTheory.tendsto_setIntegral_of_antitone

modified theorem MeasureTheory.tendsto_setIntegral_of_monotone

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem csInf_upperBounds_range

added theorem csSup_lowerBounds_range

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Antitone.ciInf_comp_tendsto_atTop

added theorem Antitone.ciInf_comp_tendsto_atTop_of_linearOrder

added theorem Antitone.ciSup_comp_tendsto_atBot

added theorem Antitone.ciSup_comp_tendsto_atBot_of_linearOrder

added theorem Antitone.iInf_comp_tendsto_atTop

added theorem Antitone.iInter_comp_tendsto_atTop

added theorem Antitone.iSup_comp_tendsto_atBot

added theorem Antitone.iUnion_comp_tendsto_atBot

added theorem Antitone.lowerBounds_range_comp_tendsto_atTop

added theorem Antitone.upperBounds_range_comp_tendsto_atBot

added theorem Monotone.ciInf_comp_tendsto_atBot

added theorem Monotone.ciInf_comp_tendsto_atBot_of_linearOrder

added theorem Monotone.ciSup_comp_tendsto_atTop

added theorem Monotone.ciSup_comp_tendsto_atTop_of_linearOrder

added theorem Monotone.iInf_comp_tendsto_atBot

added theorem Monotone.iInter_comp_tendsto_atBot

added theorem Monotone.iSup_comp_tendsto_atTop

added theorem Monotone.iUnion_comp_tendsto_atTop

added theorem Monotone.lowerBounds_range_comp_tendsto_atBot

added theorem Monotone.upperBounds_range_comp_tendsto_atTop