Zulip Chat Archive

Stream: maths

Topic: continuity and nhds


view this post on Zulip Johan Commelin (Mar 11 2019 at 11:45):

I've got the following snippet

hU : U  nhds 0
 subtype.val ⁻¹' U  nhds 0

There should be a lemma saying that if f : X → Y is continuous, and x : X and U ∈ nhds (f x), then f ⁻¹' U ∈ nhds x. But I can't find it. How do I prove such a thing?

view this post on Zulip Chris Hughes (Mar 11 2019 at 11:47):

Isn't it something like continuous_iff_tendsto

view this post on Zulip Johan Commelin (Mar 11 2019 at 11:58):

Aah, the mysterious tendsto. Thanks!


Last updated: May 18 2021 at 07:19 UTC