tendstoLocallyUniformlyOn — Mathlib

English

If F f p is locally uniform, then it is locally uniform on s.

Русский

Если локальная равномерная сходимость существует для всего пространства, то она существует на любом подмножестве.

LaTeX

$$$$\operatorname{TendstoLocallyUniformly}(F,f,p) \Rightarrow \operatorname{TendstoLocallyUniformlyOn}(F,f,p,s).$$$$

Lean4

protected theorem tendstoLocallyUniformlyOn (h : TendstoLocallyUniformly F f p) : TendstoLocallyUniformlyOn F f p s :=
  (tendstoLocallyUniformlyOn_univ.mpr h).mono (subset_univ _)

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