English
Let X be a T1 space and f : X → Y be a function into a topological space Y, with x ≠ x'. The updated function update f x y has the same value of continuity at x' as f does: ContinuousAt(update f x y) x' ⇔ ContinuousAt f x'.
Русский
Пусть X — T1-пространство и f : X → Y, где Y — топологическое пространство. При x ≠ x' функция update f x y имеет ту же непрерывность в точке x': ContinuousAt(update f x y) x' ⇔ ContinuousAt f x'.
LaTeX
$$$ \forall f:X\to Y\, \forall x,x'\in X\, \forall y\in Y,\ x'\neq x \Rightarrow \operatorname{ContinuousAt}(\mathrm{update}(f,x,y),x') \iff \operatorname{ContinuousAt}(f,x').$$$
Lean4
theorem continuousAt_update_of_ne [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : X → Y} {x x' : X} {y : Y}
(hne : x' ≠ x) : ContinuousAt (Function.update f x y) x' ↔ ContinuousAt f x' := by
simp only [← continuousWithinAt_univ, continuousWithinAt_update_of_ne hne]
