tendsto_iff_tendstoUniformly — Mathlib

English

Convergence in the metric on C0(α,β) corresponds exactly to uniform convergence of the functions on α.

Русский

Сходимость в метрике пространства C0(α,β) эквивалентна равномерной сходимости функций на α.

LaTeX

$$TendstoF_l_nhdsf_iff_TendstoUniformly: Tendsto F l (nhds f) ⇔ TendstoUniformly F f l$$

Lean4

/-- Convergence in the metric on `C₀(α, β)` is uniform convergence. -/
theorem tendsto_iff_tendstoUniformly {ι : Type*} {F : ι → C₀(α, β)} {f : C₀(α, β)} {l : Filter ι} :
    Tendsto F l (𝓝 f) ↔ TendstoUniformly (fun i => F i) f l := by
  simpa only [Metric.tendsto_nhds] using
    @BoundedContinuousFunction.tendsto_iff_tendstoUniformly _ _ _ _ _ (fun i => (F i).toBCF) f.toBCF l

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