tendstoLocallyUniformly_of_forall_exists_nhds

English

If every x has a neighborhood on which F_i tends uniformly to f, then TendstoLocallyUniformlyOn F f p s.

Русский

Если для каждого x существует окрестность внутри s, где F_i сходится равномерно к f, то выполняется TendstoLocallyUniformlyOn.

LaTeX

$$$$\forall x,\exists t\in\mathcal{N}_{s}(x), TendstoUniformlyOn F f p t \Rightarrow TendstoLocallyUniformlyOn F f p s.$$$$

Lean4

/-- If every `x` has a neighbourhood on which `F i` tends uniformly to `f`, then `F i` tends
locally uniformly to `f`. (Special case of `tendstoLocallyUniformlyOn_of_forall_exists_nhds`
where `s = univ`.) -/
theorem tendstoLocallyUniformly_of_forall_exists_nhds (h : ∀ x, ∃ t ∈ 𝓝 x, TendstoUniformlyOn F f p t) :
    TendstoLocallyUniformly F f p :=
  tendstoLocallyUniformlyOn_univ.mp <| tendstoLocallyUniformlyOn_of_forall_exists_nhds (by simpa using h)

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