English
Continuity within a set after removing a singleton equals continuity within the original set: ContinuousWithinAt f (s \ {y}) x ↔ ContinuousWithinAt f s x.
Русский
Непрерывность внутри множества после вычеркивания одинокого элемента эквивалентна непрерывности внутри исходного множества: ContinuousWithinAt f (s \ {y}) x ↔ ContinuousWithinAt f s x.
LaTeX
$$$\text{ContinuousWithinAt } f (s \{y\}) x \iff \text{ContinuousWithinAt } f s x$$$
Lean4
/-- See also `continuousWithinAt_diff_self` for the case `y = x` but not requiring `T1Space`. -/
theorem continuousWithinAt_diff_singleton [TopologicalSpace Y] [T1Space X] {x y : X} {s : Set X} {f : X → Y} :
ContinuousWithinAt f (s \ { y }) x ↔ ContinuousWithinAt f s x := by
rw [← continuousWithinAt_insert, insert_diff_singleton, continuousWithinAt_insert]
