English
On a weakly locally compact space α, convergence in the compact-open topology is equivalent to locally uniform convergence; the reverse implication holds in general.
Русский
На слабо локально компактном пространстве α схождение в топологии компактного открытия эквивалентно локально-равномерной схождению; обратное справедливо в общем случае.
LaTeX
$$$[\text{WeaklyLocallyCompactSpace } α] \Rightarrow (\text{Tendsto } F p (\mathcal{N} f) \iff \text{TendstoLocallyUniformly}(i\mapsto F(i) )(f) p)$$$
Lean4
/-- In a weakly locally compact space,
convergence in the compact-open topology is the same as locally uniform convergence.
The right-to-left implication holds in any topological space,
see `ContinuousMap.tendsto_of_tendstoLocallyUniformly`. -/
theorem tendsto_iff_tendstoLocallyUniformly [WeaklyLocallyCompactSpace α] :
Tendsto F p (𝓝 f) ↔ TendstoLocallyUniformly (fun i a => F i a) f p :=
by
refine ⟨fun h V hV x ↦ ?_, tendsto_of_tendstoLocallyUniformly⟩
rw [tendsto_iff_forall_isCompact_tendstoUniformlyOn] at h
obtain ⟨n, hn₁, hn₂⟩ := exists_compact_mem_nhds x
exact ⟨n, hn₂, h n hn₁ V hV⟩
