coeff_tendsto — Mathlib

English

For each fixed index d, the coefficient map f ↦ f.d is uniformly continuous on Laurent series with respect to the uniform structure; this holds for any base K.

Русский

Для фиксированного коэффициента d отображение f ↦ f_d равно по униформной топологии непрерывности на рядах Лаурента.

LaTeX

$$$\text{UniformContinuous}(\lambda f. f_{d})$$$

Lean4

theorem coeff_tendsto {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) (D : ℤ) :
    Tendsto (fun f : K⸨X⸩ ↦ f.coeff D) ℱ (𝓟 {coeff hℱ D}) :=
  let _ : UniformSpace K := ⊥
  le_of_eq <| DiscreteUniformity.eq_pure_cauchyConst (hℱ.map (uniformContinuous_coeff D)) ▸ (principal_singleton _).symm

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