continuity and nhds

Stream: maths

[Johan Commelin]

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]

Isn't it something like continuous_iff_tendsto

[Johan Commelin]

Aah, the mysterious tendsto. Thanks!