tendsto_iff_tendstoUniformly — Mathlib

English

If α is compact, convergence in the compact-open topology is equivalent to convergence uniformly on α.

Русский

Если α компактно, то схождение в топологии компактного открытия эквивалентно равномерной сходжения по α.

LaTeX

$$$[\text{CompactSpace } α] \Rightarrow \text{Tendsto } F p (\mathcal{N} f) \iff \text{TendstoUniformly } (i \mapsto F(i)) f p$$$

Lean4

/-- Convergence in the compact-open topology is the same as uniform convergence for sequences of
continuous functions on a compact space. -/
theorem tendsto_iff_tendstoUniformly : Tendsto F p (𝓝 f) ↔ TendstoUniformly (fun i a => F i a) f p := by
  simp [isUniformEmbedding_uniformFunOfFun.isInducing.tendsto_nhds_iff, UniformFun.tendsto_iff_tendstoUniformly,
    Function.comp_def]

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