Zulip Chat Archive
Stream: PR reviews
Topic: 3454 add `ne_bot`
Yury G. Kudryashov (Jul 19 2020 at 14:46):
In #3454 I add a typeclass filter.ne_bot and use it in many lemmas. The goal is to avoid nhds_ne_bot/at_top_ne_bot in lemmas like tendsto_nhds_unique and tendsto.lim_eq.
Last updated: May 02 2025 at 03:31 UTC