Limit on neighborhood from punctured neighborhood

Stream: Is there code for X?

[Michael Stoll]

How to prove the following?

import Mathlib

open Filter Topology in
example (f : ℂ → ℂ) (w z : ℂ) (h₁ : Tendsto f (𝓝[≠] w) (𝓝 z)) (h₂ : f w = z) :
    Tendsto f (𝓝 w) (𝓝 z) := by sorry

[Michael Stoll]

@loogle (Filter.Tendsto ?f (nhdsWithin ?w ?_) (nhds ?z)), (Filter.Tendsto ?f (nhds ?w) (nhds ?z))

[loogle]

:shrug: nothing found

[Yaël Dillies]

Why not just rewrite h₂?

[Michael Stoll]

So, how to prove

import Mathlib

open Filter Topology in
example (f : ℂ → ℂ) (w : ℂ) (h₁ : Tendsto f (𝓝[≠] w) (𝓝 (f w))) :
    Tendsto f (𝓝 w) (𝓝 (f w)) := by sorry

then? (Still no match in Loogle.)

[Michael Stoll]

Ah: docs#continuousWithinAt_compl_self .

[Michael Stoll]

Need to write this as a continuity statement (which is what I came from originally).

[Anatole Dedecker]

You can also rewrite using docs#nhdsWithin_compl_singleton_sup_pure and docs#Filter.tendsto_sup, and then use docs#tendsto_pure_nhds