tendstoLocallyUniformlyOn_iff_forall_isCompact

English

Locally compact spaces support equivalences between various formulations of local uniform convergence.

Русский

Локально компактные пространства поддерживают эквивалентности между различными формулировками локальной равномерной сходимости.

LaTeX

$$$$[LocallyCompactSpace\ α] \Rightarrow (TendstoLocallyUniformlyOn F f p s \iff \forall K, K\subset s, IsCompact K \Rightarrow TendstoUniformlyOn F f p K).$$$$

Lean4

theorem tendstoLocallyUniformlyOn_iff_forall_isCompact [LocallyCompactSpace α] (hs : IsOpen s) :
    TendstoLocallyUniformlyOn F f p s ↔ ∀ K, K ⊆ s → IsCompact K → TendstoUniformlyOn F f p K :=
  (tendstoLocallyUniformlyOn_TFAE F f p hs).out 0 1

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