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