tendsto_at — Mathlib

English

Equivalence expressing TendstoUniformlyOn in terms of the coercion to the subtype.

Русский

Эквивалентность выражения TendstoUniformlyOn через приведение к подптипу.

LaTeX

$$$$TendstoUniformlyOn F f p s\\iff TendstoUniformly (\\lambda i x: F i x) (f \\circ (Subtype.val)) p.$$$$

Lean4

/-- Uniform convergence implies pointwise convergence. -/
theorem tendsto_at (h : TendstoUniformlyOn F f p s) (hx : x ∈ s) : Tendsto (fun n => F n x) p <| 𝓝 (f x) :=
  h.tendstoUniformlyOnFilter.tendsto_at (le_principal_iff.mpr <| mem_principal.mpr <| singleton_subset_iff.mpr <| hx)

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