English
If two sets coincide around x except possibly at y, then continuity within one set at x is equivalent to continuity within the other.
Русский
Если два множества совпадают вокруг x за исключением y, то непрерывность внутри одного множества в x эквивалентна непрерывности внутри другого.
LaTeX
$$$\text{ContinuousWithinAt } f s x \iff \text{ContinuousWithinAt } f t x$ given h: s =ᶠ[\mathcal{N}[\{ y \}^c] x] t$$
Lean4
/-- If two sets coincide locally around `x`, except maybe at `y`, then it is equivalent to be
continuous at `x` within one set or the other. -/
theorem continuousWithinAt_congr_set' [TopologicalSpace Y] [T1Space X] {x : X} {s t : Set X} {f : X → Y} (y : X)
(h : s =ᶠ[𝓝[{ y }ᶜ] x] t) : ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x :=
by
rw [← continuousWithinAt_insert_self (s := s), ← continuousWithinAt_insert_self (s := t)]
exact continuousWithinAt_congr_set (eventuallyEq_insert h)
