Commit 2024-11-22 00:49 ff67e337

View on Github →

chore(Topology/Order): move&generalize 4 lemmas (#19238) Generalize lemmas from CompleteLinearOrder to ConditionallyCompleteLattice or ConditionallyCompleteLinearOrder.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

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

deleted theorem iInf_eq_of_forall_le_of_tendsto

deleted theorem iSup_eq_of_forall_le_of_tendsto

deleted theorem iUnion_Ici_eq_Ioi_of_lt_of_tendsto

deleted theorem iUnion_Iic_eq_Iio_of_lt_of_tendsto

Modified Mathlib/Topology/Order/OrderClosed.lean

added theorem IsGLB.range_of_tendsto

added theorem IsLUB.range_of_tendsto

added theorem iInf_eq_of_forall_le_of_tendsto

added theorem iSup_eq_of_forall_le_of_tendsto

added theorem iUnion_Ici_eq_Ioi_of_lt_of_tendsto

added theorem iUnion_Iic_eq_Iio_of_lt_of_tendsto