Commit 2023-08-14 12:01 a6b1311d

View on Github →

chore: move lemmas from Stietljes.lean to their proper afterport places (#6554)

Estimated changes

Modified Mathlib/Data/Real/Basic.lean

added theorem Real.iInf_Ioi_eq_iInf_rat_gt

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.tendsto_measure_Ici_atBot

added theorem MeasureTheory.tendsto_measure_Ico_atTop

added theorem MeasureTheory.tendsto_measure_Iic_atTop

added theorem MeasureTheory.tendsto_measure_Ioc_atBot

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

deleted theorem MeasureTheory.tendsto_measure_Ici_atBot

deleted theorem MeasureTheory.tendsto_measure_Ico_atTop

deleted theorem MeasureTheory.tendsto_measure_Iic_atTop

deleted theorem MeasureTheory.tendsto_measure_Ioc_atBot

deleted theorem exists_seq_antitone_tendsto_atTop_atBot

deleted theorem exists_seq_monotone_tendsto_atTop_atTop

deleted theorem iInf_Ioi_eq_iInf_rat_gt

deleted theorem iSup_eq_iSup_subseq_of_antitone

deleted theorem rightLim_eq_of_tendsto

deleted theorem rightLim_eq_sInf

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Filter.exists_seq_antitone_tendsto_atTop_atBot

added theorem Filter.exists_seq_monotone_tendsto_atTop_atTop

Modified Mathlib/Probability/Kernel/CondCdf.lean

Modified Mathlib/Topology/Algebra/Order/LeftRightLim.lean

added theorem Monotone.rightLim_eq_sInf

added theorem rightLim_eq_of_eq_bot

added theorem rightLim_eq_of_tendsto

Modified Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean

added theorem iInf_eq_iInf_subseq_of_antitone

added theorem iSup_eq_iSup_subseq_of_antitone