Commit 2023-11-01 12:39 36a2a825

View on Github →

feat: Eventual boundedness of neighborhoods (#8009) Forward port https://github.com/leanprover-community/mathlib/pull/18629

Estimated changes

Modified Mathlib/Order/Filter/Pi.lean

added theorem Filter.Eventually.eval_pi

added theorem Filter.eventually_pi

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

modified theorem Filter.Tendsto.bddAbove_range

modified theorem Filter.Tendsto.bddAbove_range_of_cofinite

modified theorem Filter.Tendsto.bddBelow_range

modified theorem Filter.Tendsto.bddBelow_range_of_cofinite

modified theorem Filter.Tendsto.isBoundedUnder_ge

modified theorem Filter.Tendsto.isBoundedUnder_le

modified theorem Filter.Tendsto.isCoboundedUnder_ge

modified theorem Filter.Tendsto.isCoboundedUnder_le

modified theorem iUnion_Ici_eq_Ioi_of_lt_of_tendsto

modified theorem iUnion_Iic_eq_Iio_of_lt_of_tendsto