English
Let X be a T1 space and f : X → Y. For any subset s ⊆ X and points x ∈ X and y ∈ Y, ContinuousOn (update f x y) s holds if and only if ContinuousOn f on s \\ {x} and, whenever x ∈ s, Tendsto f along 𝓝[s \\ {x}] x to 𝓝 y.
Русский
Пусть X — T1-пространство и f : X → Y. Для множества s ⊆ X и точек x ∈ X, y ∈ Y верно: ContinuousOn (update f x y) s тогда и только тогда, когда ContinuousOn f на s \\ {x} и при x ∈ s выполняется Tendsto f от 𝓝[s \\ {x}] x к 𝓝 y.
LaTeX
$$$ \\text{ContinuousOn}(\\mathrm{update}(f,x,y),s) \\iff \\left( \\text{ContinuousOn}(f,\,s\\setminus\\{x\\}) \\land (x\\in s \\to \\operatorname{Tendsto} f (\\mathcal{N}_{s\\setminus\\{x\\}} x) (\\mathcal{N} y))\\right).$$$
Lean4
theorem continuousOn_update_iff [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {x : X}
{y : Y} :
ContinuousOn (Function.update f x y) s ↔ ContinuousOn f (s \ { x }) ∧ (x ∈ s → Tendsto f (𝓝[s \ { x }] x) (𝓝 y)) :=
by
rw [ContinuousOn, ← and_forall_ne x, and_comm]
refine and_congr ⟨fun H z hz => ?_, fun H z hzx hzs => ?_⟩ (forall_congr' fun _ => ?_)
· specialize H z hz.2 hz.1
rw [continuousWithinAt_update_of_ne hz.2] at H
exact H.mono diff_subset
· rw [continuousWithinAt_update_of_ne hzx]
refine (H z ⟨hzs, hzx⟩).mono_of_mem_nhdsWithin (inter_mem_nhdsWithin _ ?_)
exact isOpen_ne.mem_nhds hzx
· exact continuousWithinAt_update_same
