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 _.
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 _.