tendsto_at — Mathlib

English

Equivalence between TendstoUniformlyOnFilter and the corresponding Tendsto to the uniformity.

Русский

Эквивалентность между TendstoUniformlyOnFilter и стремлением к равномерности.

LaTeX

$$$$TendstoUniformlyOnFilter F f p p'\\iff Tendsto(\\lambda q: { fst:=f q.snd, snd:= F q.fst q.snd }) (Filter.instSProd.sprod p p') (uniformity(β)).$$$$

Lean4

/-- Uniform convergence implies pointwise convergence. -/
theorem tendsto_at (h : TendstoUniformlyOnFilter F f p p') (hx : 𝓟 { x } ≤ p') :
    Tendsto (fun n => F n x) p <| 𝓝 (f x) :=
  by
  refine Uniform.tendsto_nhds_right.mpr fun u hu => mem_map.mpr ?_
  filter_upwards [(h u hu).curry]
  intro i h
  simpa using h.filter_mono hx

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