English
In a Frechet-Urysohn space, convergence of a function is equivalent to its sequential convergence: Tendsto f (nhds a) (nhds b) holds iff for every sequence u_n → a, Tendsto (f ∘ u) → b.
Русский
В пространстве Фреше–Ури́шхо́н схождение функции эквивалентно последовательностному схождению: Tendsto f (nhds a) (nhds b) эквивалентно для каждой последовательности u_n → a имеет место Tendsto (f ∘ u) → b.
LaTeX
$$$\mathrm{Tendsto}\ f\ (\mathcal{N}(a))\ (\mathcal{N}(b)) \iff \forall u:\mathbb{N}\to X,\ Tendsto u\ atTop\ (\mathcal{N}(a)) \rightarrow \ Tendsto (f \circ u)\ atTop\ (\mathcal{N}(b))$$$
Lean4
/-- If the domain of a function `f : α → β` is a Fréchet-Urysohn space, then convergence
is equivalent to sequential convergence. See also `Filter.tendsto_iff_seq_tendsto` for a version
that works for any pair of filters assuming that the filter in the domain is countably generated.
This property is equivalent to the definition of `FrechetUrysohnSpace`, see
`FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto`. -/
theorem tendsto_nhds_iff_seq_tendsto [FrechetUrysohnSpace X] {f : X → Y} {a : X} {b : Y} :
Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ u : ℕ → X, Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b) :=
by
refine ⟨fun hf u hu => hf.comp hu, fun h => ((nhds_basis_closeds _).tendsto_iff (nhds_basis_closeds _)).2 ?_⟩
rintro s ⟨hbs, hsc⟩
refine ⟨closure (f ⁻¹' s), ⟨mt ?_ hbs, isClosed_closure⟩, fun x => mt fun hx => subset_closure hx⟩
rw [← seqClosure_eq_closure]
rintro ⟨u, hus, hu⟩
exact hsc.mem_of_tendsto (h u hu) (Eventually.of_forall hus)
