tendstoUniformlyOnFilter_const — Mathlib

English

If a sequence g converges to b along p, then the sequence of constant functions mapping every input to g(n) converges uniformly on p to the constant function b on any p'.

Русский

Если последовательность g сходится к b по p, то последовательность констант g(n) сходится равномерно по p к константе b на любом p'.

LaTeX

$$TendstoUniformlyOnFilter (fun n => fun _ => g n) (fun _ => b) p p'$$

Lean4

/-- If a sequence `g` converges to some `b`, then the sequence of constant functions
`fun n ↦ fun a ↦ g n` converges to the constant function `fun a ↦ b` on any set `s` -/
theorem tendstoUniformlyOnFilter_const {g : ι → β} {b : β} (hg : Tendsto g p (𝓝 b)) (p' : Filter α) :
    TendstoUniformlyOnFilter (fun n : ι => fun _ : α => g n) (fun _ : α => b) p p' := by
  simpa only [nhds_eq_comap_uniformity, tendsto_comap_iff] using hg.comp (tendsto_fst (g := p'))

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