Continuous of neighborhoods

Stream: Is there code for X?

[Aaron Liu]

I want to prove a function is continuous from its action on neighborhoods, so the converse to docs#Continuous.tendsto. I couldn't find this theorem anywhere.

import Mathlib

example {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y}
    (hf : ∀ x : X, Filter.Tendsto f (nhds x) (nhds (f x))) : Continuous f := by
  sorry

[Junyan Xu]

hf x is it's the definition of ContinuousAt

[Aaron Liu]

Is that meant to be unfolded?

[Junyan Xu]

(so you can use continuous_iff_continuousAt)
(I think the answer is you should stick to the ContinuousAt API rather than unfolding it)

[Aaron Liu]

If I don't want to unfold it then how do I get ContinuousAt x ↔ Filter.Tendsto f (nhds x) (nhds (f x))?

[Kenny Lau]

@Aaron Liu ContinuousAt.tendsto

[Kenny Lau]

and continuousAt_of_tendsto_nhds for the other direction

[Aaron Liu]

No I want the other direction

[Aaron Liu]

Kenny Lau said:

and continuousAt_of_tendsto_nhds for the other direction

1. This needs T1Space (which is not a problem for me but I thought I'd mention it anyways)
2. It's very annoying to use this with apply since I get ?y in my goal

[Aaron Liu]

For context, I want to prove a function partially defined on a quotient (so from a subtype of a quotient) is continuous, so it's much easier to work with neighborhoods since then I can use lemmas like docs#nhds_subtype.

[Anatole Dedecker]

With the current API unfolding is the best solution.