Commit 2025-04-28 13:10 203cf538

View on Github →

refactor: generalize unbounded_of_tendsto_atTop (#23531)

Estimated changes

Modified Mathlib/Order/Filter/AtTopBot/Basic.lean

added theorem Filter.not_bddAbove_of_tendsto_atTop

added theorem Filter.not_bddBelow_of_tendsto_atBot

deleted theorem Filter.unbounded_of_tendsto_atBot'

deleted theorem Filter.unbounded_of_tendsto_atBot

deleted theorem Filter.unbounded_of_tendsto_atTop'

deleted theorem Filter.unbounded_of_tendsto_atTop

Modified Mathlib/Probability/Martingale/BorelCantelli.lean