tendstoLocallyUniformly_iff_filter

English

On a compact space, locally uniform convergence is equivalent to uniform convergence.

Русский

На компактном пространстве локальная равномерная сходимость эквивалентна равномерной.

LaTeX

$$$$[CompactSpace\ α] \Rightarrow (TendstoLocallyUniformly F f p \iff TendstoUniformly F f p).$$$$

Lean4

theorem tendstoLocallyUniformly_iff_filter :
    TendstoLocallyUniformly F f p ↔ ∀ x, TendstoUniformlyOnFilter F f p (𝓝 x) := by
  simpa [← tendstoLocallyUniformlyOn_univ, ← nhdsWithin_univ] using
    @tendstoLocallyUniformlyOn_iff_filter _ _ _ _ _ F f univ p

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