English
Let f,g: α → β and s ⊆ α, a ∈ α, l a filter on β. If f and g agree on s, and f tends to l along the nhdsWithin a of s, then g tends to l along the same nhdsWithin.
Русский
Пусть f, g : α → β и s ⊆ α, a ∈ α, l фильтр на β. Если f и g совпадают на s, и f стремится к l вдоль nhdsWithin a относительно s, то и g стремится к l вдоль того же nhdsWithin.
LaTeX
$$$ (\\\\forall x \\\\in s, f x = g x) \\\\rightarrow Tendsto f (\\\\mathcal{N} [s] a) l \\\\rightarrow Tendsto g (\\\\mathcal{N} [s] a) l $$$
Lean4
theorem tendsto_nhdsWithin_congr {f g : α → β} {s : Set α} {a : α} {l : Filter β} (hfg : ∀ x ∈ s, f x = g x)
(hf : Tendsto f (𝓝[s] a) l) : Tendsto g (𝓝[s] a) l :=
(tendsto_congr' <| eventuallyEq_nhdsWithin_of_eqOn hfg).1 hf
