English
Let f: α → β be a function between topological spaces, x ∈ α, y ∈ β. The function update f x y is continuous at x if and only if f tends to y along the punctured neighborhood of x, i.e., along 𝓝[≠] x.
Русский
Пусть f: α → β — функция между топологическими пространствами, x ∈ α, y ∈ β. Функция update f x y непрерывна в точке x тогда и только тогда, когда f стремится к y по окружению x с вычитанием самой точки x, то есть вдоль 𝓝[≠] x.
LaTeX
$$$\operatorname{ContinuousAt}(\mathrm{update}(f,x,y), x) \iff \operatorname{Tendsto} f\bigl( \mathcal{N}_{x}^{\neq} \bigr) \bigl( \mathcal{N}_{y} \bigr).$$$
Lean4
@[simp]
theorem continuousAt_update_same [DecidableEq α] {y : β} :
ContinuousAt (Function.update f x y) x ↔ Tendsto f (𝓝[≠] x) (𝓝 y) := by
rw [← continuousWithinAt_univ, continuousWithinAt_update_same, compl_eq_univ_diff]
