Zulip Chat Archive

Stream: Is there code for X?

Topic: continuous.of_locally_constant


view this post on Zulip 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?

view this post on Zulip Floris van Doorn (Apr 05 2021 at 19:37):

docs#is_locally_constant.iff_continuous

view this post on Zulip Floris van Doorn (Apr 05 2021 at 19:49):

By the way, the search function of the docs is very useful:
https://leanprover-community.github.io/mathlib_docs/find/Do_we_have_a_lemma_saying_that_a_map_to_a_discrete_space_is_continuous_if_and_only_if_it's_locally_constant

view this post on Zulip Adam Topaz (Apr 05 2021 at 19:52):

I just get a 404 error with that link

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Apr 05 2021 at 19:55):

I'm on mobile, that could be the issue

view this post on Zulip 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.

view this post on Zulip 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