English
Continuity within a set is unchanged if we insert a point y different from x: ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x (provided x ≠ y).
Русский
Непрерывность внутри множества не изменяется при добавлении точки y, если x ≠ y: ContinuousWithinAt f (insert y s) x ⇔ ContinuousWithinAt f s x.
LaTeX
$$$\text{ContinuousWithinAt } f(\mathrm{insert}\, y\, s)\ x \iff \text{ContinuousWithinAt } f\ s\ x$ (при x ≠ y)$$
Lean4
theorem continuousWithinAt_insert [TopologicalSpace Y] [T1Space X] {x y : X} {s : Set X} {f : X → Y} :
ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x :=
by
rcases eq_or_ne x y with (rfl | h)
· exact continuousWithinAt_insert_self
simp_rw [ContinuousWithinAt, nhdsWithin_insert_of_ne h]
