tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact

English

For LocallyCompact spaces, local uniform convergence on a compact set is equivalent to uniform convergence on that set.

Русский

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

LaTeX

$$$$\text{IsCompact}(s) \Rightarrow (\operatorname{TendstoLocallyUniformlyOn} F f p s \iff \operatorname{TendstoUniformlyOn} F f p s).$$$$

Lean4

/-- For a compact set `s`, locally uniform convergence on `s` is just uniform convergence on `s`. -/
theorem tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact (hs : IsCompact s) :
    TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s :=
  by
  haveI : CompactSpace s := isCompact_iff_compactSpace.mp hs
  refine ⟨fun h => ?_, TendstoUniformlyOn.tendstoLocallyUniformlyOn⟩
  rwa [tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe,
    tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace, ←
    tendstoUniformlyOn_iff_tendstoUniformly_comp_coe] at h

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