tendsto_at — Mathlib

English

There is a local uniform convergence criterion via pointwise convergence on nhdsWithin x.

Русский

Существует критерий локальной равномерной сходимости через точечное сходимость в nhdsWithin x.

LaTeX

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

Lean4

theorem tendsto_at (hf : TendstoLocallyUniformlyOn F f p s) {a : α} (ha : a ∈ s) :
    Tendsto (fun i => F i a) p (𝓝 (f a)) :=
  by
  refine ((tendstoLocallyUniformlyOn_iff_filter.mp hf) a ha).tendsto_at ?_
  simpa only [Filter.principal_singleton] using pure_le_nhdsWithin ha

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