English
Let X be a T1 space, Y a topological space, and f : X → Y. For any s ⊆ X, and any x, x' ∈ X with x' ≠ x, and any y ∈ Y, the function obtained by updating f at x to y has the same continuity within s at x' as f does; i.e., ContinuousWithinAt(update f x y) s x' ⇔ ContinuousWithinAt f s x'.
Русский
Пусть X — T1-пространство, Y — топологическое пространство, и f : X → Y. Для любого s ⊆ X и любых x, x' ∈ X с x' ≠ x, и любого y ∈ Y функция, полученная путем замены значения f(x) на y, имеет ту же непрерывность внутри s в точке x', что и f; то есть ContinuousWithinAt(update f x y) s x' ⇔ ContinuousWithinAt f s x'.
LaTeX
$$$ \forall f:X\to Y\, \forall s\subseteq X\, \forall x,x'\in X\, \forall y\in Y,\ x'\neq x \Rightarrow \operatorname{ContinuousWithinAt}(\mathrm{update}(f,x,y))\,s\,x' \iff \operatorname{ContinuousWithinAt}(f\,s\,x').$$$
Lean4
theorem continuousWithinAt_update_of_ne [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : X → Y} {s : Set X}
{x x' : X} {y : Y} (hne : x' ≠ x) : ContinuousWithinAt (Function.update f x y) s x' ↔ ContinuousWithinAt f s x' :=
EventuallyEq.congr_continuousWithinAt
(mem_nhdsWithin_of_mem_nhds <|
mem_of_superset (isOpen_ne.mem_nhds hne) fun _y' hy' => Function.update_of_ne hy' _ _)
(Function.update_of_ne hne ..)
