tendstoUniformlyOn_singleton_iff_tendsto

English

Uniform convergence on a singleton {x} is equivalent to ordinary convergence of the sequence F_n x to f x in the ambient space.

Русский

Равномерная сходимость на синглетоне {x} эквивалентна обычной сходимости F_n x к f x в пространстве.

LaTeX

$$TendstoUniformlyOn F f p { x } ↔ Tendsto (fun n : ι => F n x) p (𝓝 (f x))$$

Lean4

/-- Uniform convergence on a singleton is equivalent to regular convergence -/
theorem tendstoUniformlyOn_singleton_iff_tendsto :
    TendstoUniformlyOn F f p { x } ↔ Tendsto (fun n : ι => F n x) p (𝓝 (f x)) :=
  by
  simp_rw [tendstoUniformlyOn_iff_tendsto, Uniform.tendsto_nhds_right, tendsto_def]
  exact forall₂_congr fun u _ => by simp [preimage]

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