English
Let f, g: X → Y be functions between topological spaces, and s ⊆ X with x ∈ s. If f is continuous at x relative to s and g agrees with f on some neighborhood of x within s (i.e., g and f are eventually equal near x with respect to nhdsWithin x s), then g is also continuous at x relative to s.
Русский
Пусть f, g: X → Y — функции между топологическими пространствами, s ⊆ X и x ∈ s. Если f непрерывна в точке x относительно множества s, и g совпадает с f на некотором окрестности x внутри s (то есть g и f совпадают локально по отношению к 𝓝[x] ∩ s), то и g непрерывна в x относительно s.
LaTeX
$$$ \text{Let } X,Y \text{ be topological spaces},\ f,g: X\to Y,\ s\subseteq X,\ x\in s.\ When\ f|_s\text{ is continuous at }x\text{ and }\exists U\in \mathcal{N}(x):U\subseteq s\land \forall y\in U\ g(y)=f(y),\ then\\ g|_s\text{ is continuous at }x.$$$
Lean4
theorem congr_of_eventuallyEq_of_mem (h : ContinuousWithinAt f s x) (h₁ : g =ᶠ[𝓝[s] x] f) (hx : x ∈ s) :
ContinuousWithinAt g s x :=
h.congr_of_eventuallyEq h₁ (mem_of_mem_nhdsWithin hx h₁ :)
