English
If s and t coincide around x, then ContinuousWithinAt f s x and ContinuousWithinAt f t x are equivalent.
Русский
Если окрестности s и t совпадают вокруг x, то непрерывность внутри них одинакова.
LaTeX
$$$s =^\\!\\!_{\\mathcal{N}x} t \\Rightarrow (ContinuousWithinAt f s x \\leftrightarrow ContinuousWithinAt f t x)$$$
Lean4
/-- If two sets coincide around `x`, then being continuous within one or the other at `x` is
equivalent. See also `continuousWithinAt_congr_set'` which requires that the sets coincide
locally away from a point `y`, in a T1 space. -/
theorem continuousWithinAt_congr_set (h : s =ᶠ[𝓝 x] t) : ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x := by
simp only [ContinuousWithinAt, nhdsWithin_eq_iff_eventuallyEq.mpr h]
