tendstoLocallyUniformly_iff_forall_isCompact

English

Locally uniform convergence on s is equivalent to uniform convergence with respect to the filter 𝓝[s] x for each x ∈ s.

Русский

Локальная равномерная сходимость на s эквивалентна равномерной сходимости по фильтру 𝓝[s] x для каждой x ∈ s.

LaTeX

$$$$\operatorname{TendstoLocallyUniformlyOn}(F,f,p,s) \iff \forall x \in s,\ TendstoUniformlyOnFilter(F,f,p,(\mathcal{N}_{s} x)).$$$$

Lean4

theorem tendstoLocallyUniformly_iff_forall_isCompact [LocallyCompactSpace α] :
    TendstoLocallyUniformly F f p ↔ ∀ K : Set α, IsCompact K → TendstoUniformlyOn F f p K := by
  simp only [← tendstoLocallyUniformlyOn_univ, tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_univ,
    Set.subset_univ, forall_true_left]

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