English
Let f: α → β be a function between topological spaces, x ∈ α, y ∈ β, and s ⊆ α. The function update f x y, which coincides with f away from x and takes the value y at x, is continuous at x with respect to the set s if and only if f tends to y along the nhds of x restricted to s \ {x}. In other words, the updated function is continuous at x exactly when the original function f approaches y along all paths staying in s except possibly at x.
Русский
Пусть f: α → β — функция между топологическими пространствами, x ∈ α, y ∈ β и s ⊆ α. Функция update f x y, которая равна f вне точки x и принимает значение y в точке x, непрерывна в точке x относительно множества s тогда и только тогда, когда f стремится к y вдоль окружения x, ограниченного множеством s \ {x}. Иными словами, обновленная функция непрерывна в x тогда и только тогда, когда f стремится к y по всем путям, остающимся в s за исключением точки x.
LaTeX
$$$\\operatorname{ContinuousWithinAt}(\\mathrm{update}(f,x,y), s, x) \\iff \\operatorname{Tendsto} f\\bigl( \\mathcal{N}_{x}^{\,s \\setminus \\{x\\}} \\bigr) \\bigl( \\mathcal{N}_{y} \\bigr).$$$
Lean4
@[simp]
theorem continuousWithinAt_update_same [DecidableEq α] {y : β} :
ContinuousWithinAt (update f x y) s x ↔ Tendsto f (𝓝[s \ { x }] x) (𝓝 y) :=
calc
ContinuousWithinAt (update f x y) s x ↔ Tendsto (update f x y) (𝓝[s \ { x }] x) (𝓝 y) := by {
rw [← continuousWithinAt_diff_self, ContinuousWithinAt, update_self]
}
_ ↔ Tendsto f (𝓝[s \ { x }] x) (𝓝 y) :=
tendsto_congr' <| eventually_nhdsWithin_iff.2 <| Eventually.of_forall fun _ hz => update_of_ne hz.2 ..
