continuous.of_locally_constant

Stream: Is there code for X?

[Adam Topaz]

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]

docs#is_locally_constant.iff_continuous

[Floris van Doorn]

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

[Adam Topaz]

I just get a 404 error with that link

[Adam Topaz]

Thanks for the lemma though! Johan actually mentioned this one to me shortly after I posted yesterday

[Floris van Doorn]

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]

I'm on mobile, that could be the issue

[Floris van Doorn]

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]

Yeah it's working on desktop. But strangely it doesn't work on mobile even with the desktop site...