tendsto_of_tendstoLocallyUniformly

English

If a net F indexed by i converges locally uniformly to f, then F converges to f in the compact-open topology.

Русский

Если сеть F инициируется локально равномерно к f, то F сходится к f в топологии компактного открытия.

LaTeX

$$$\text{TendstoLocallyUniformly}((i,a)\mapsto F(i)a)\; f\; p \Rightarrow \text{Tendsto } F\; p\; (\mathcal{N} f)$$$

Lean4

/-- Locally uniform convergence implies convergence in the compact-open topology. -/
theorem tendsto_of_tendstoLocallyUniformly (h : TendstoLocallyUniformly (fun i a => F i a) f p) : Tendsto F p (𝓝 f) :=
  by
  rw [tendsto_iff_forall_isCompact_tendstoUniformlyOn]
  intro K hK
  rw [← tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK]
  exact h.tendstoLocallyUniformlyOn

Похожие утверждения