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).
Last updated: May 17 2021 at 16:26 UTC