Stream: Is there code for X?
Adam Topaz (Apr 04 2021 at 18:37):
Do we have a lemma saying that a map to a discrete space is continuous if and only if it's locally constant?
Floris van Doorn (Apr 05 2021 at 19:37):
Floris van Doorn (Apr 05 2021 at 19:49):
By the way, the search function of the docs is very useful:
Adam Topaz (Apr 05 2021 at 19:52):
I just get a 404 error with that link
Adam Topaz (Apr 05 2021 at 19:53):
Thanks for the lemma though! Johan actually mentioned this one to me shortly after I posted yesterday
Floris van Doorn (Apr 05 2021 at 19:54):
Oh, I get a list of suggestions, which includes the lemma I mention.
More partically: if you search for a lemma it usually works if you search for the terms in your lemma separated by underscores: https://leanprover-community.github.io/mathlib_docs/find/discrete_space_continuous_locally_constant
(hopefully that link works)
Adam Topaz (Apr 05 2021 at 19:55):
I'm on mobile, that could be the issue
Floris van Doorn (Apr 05 2021 at 20:03):
On a desktop you have to wait a couple of seconds before it shows a list of suggestions. But maybe this doesn't work on mobile.
Adam Topaz (Apr 05 2021 at 20:07):
Yeah it's working on desktop. But strangely it doesn't work on mobile even with the desktop site...
Last updated: May 16 2021 at 05:21 UTC