Zulip Chat Archive
Stream: Is there code for X?
Topic: Moore-Smith sequences
Pedro Minicz (Sep 23 2020 at 14:39):
Do we have nets in mathlib?
Pedro Minicz (Sep 23 2020 at 14:40):
I believe it may be defined in terms of filters somewhere.
Reid Barton (Sep 23 2020 at 14:59):
As far as I know, we don't have them (and use filters instead where one might use nets).
ZHAO Jinxiang (Aug 25 2022 at 17:14):
So we have no "net" in mathlib now? :flushed:
ZHAO Jinxiang (Aug 25 2022 at 17:20):
Also, is there anything called directed set?
Yaël Dillies (Aug 25 2022 at 17:21):
Patrick Massot (Aug 25 2022 at 17:23):
Everywhere nets could be used we use filters that are much more versatile.
Last updated: Dec 20 2023 at 11:08 UTC