## Stream: maths

### Topic: continuity and nhds

#### 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?

#### Chris Hughes (Mar 11 2019 at 11:47):

Isn't it something like continuous_iff_tendsto

#### Johan Commelin (Mar 11 2019 at 11:58):

Aah, the mysterious tendsto. Thanks!

Last updated: May 18 2021 at 07:19 UTC