Commit 2024-10-05 06:02 875821f5

View on Github →

feat(Filter/AtTopBot): add atTop_neBot_iff (#17428) I'm going to use these lemmas to drop [Nonempty α] and [IsDirected α (· ≤ ·)] assumptions in lemmas asserting Tendsto _ atTop _.

Estimated changes