English
If a function f into a T1 space tends to a limit y along nhds x, then f(x) = y.
Русский
Если функция f в T1-пространство стремится к пределy y вдоль окрестностей x, то f(x) = y.
LaTeX
$$$\text{Tendsto } f (\mathcal{N} x) (\mathcal{N} y) \Rightarrow f(x) = y$$$
Lean4
/-- If a function to a `T1Space` tends to some limit `y` at some point `x`, then necessarily
`y = f x`. -/
theorem eq_of_tendsto_nhds [TopologicalSpace Y] [T1Space Y] {f : X → Y} {x : X} {y : Y} (h : Tendsto f (𝓝 x) (𝓝 y)) :
f x = y :=
by_contra fun hfa : f x ≠ y =>
have fact₁ : {f x}ᶜ ∈ 𝓝 y := compl_singleton_mem_nhds hfa.symm
have fact₂ : Tendsto f (pure x) (𝓝 y) := h.comp (tendsto_id'.2 <| pure_le_nhds x)
fact₂ fact₁ (Eq.refl <| f x)
