English
Let a ∈ α, s ⊆ α, f: β → α, l a filter. The convergence of f to a within s is equivalent to f converging to a in the ambient space and f(n) eventually landing in s.
Русский
Пусть a ∈ α, s ⊆ α, f: β → α и l — фильтр. Сходимость f к a внутри s эквивалентна сходимости f к a в пространстве и тому, что значения f(n) в большинстве случаев попадают в s.
LaTeX
$$$ Tendsto f l (\\mathcal{N} [s] a) \\iff \\ Tendsto f l (\\mathcal{N} a) \\wedge \\ forall^\\infty n \\in l, f n \\in s $$$
Lean4
theorem tendsto_nhdsWithin_iff {a : α} {l : Filter β} {s : Set α} {f : β → α} :
Tendsto f l (𝓝[s] a) ↔ Tendsto f l (𝓝 a) ∧ ∀ᶠ n in l, f n ∈ s :=
⟨fun h => ⟨tendsto_nhds_of_tendsto_nhdsWithin h, eventually_mem_of_tendsto_nhdsWithin h⟩, fun h =>
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ h.1 h.2⟩
