comp_tendstoUniformly — Mathlib

English

If g is uniformly continuous and TendstoUniformly F f p holds, then TendstoUniformly (g ∘ F) (g ∘ f) p holds.

Русский

Если g равномерно непрерывна и F сходится равномерно к f, то g∘F сходится равномерно к g∘f.

LaTeX

$$hg : UniformContinuous g ⇒ (h : TendstoUniformly F f p) ⇒ TendstoUniformly (fun i => g ∘ F i) (g ∘ f) p$$

Lean4

/-- Composing on the left by a uniformly continuous function preserves uniform convergence -/
theorem comp_tendstoUniformly [UniformSpace γ] {g : β → γ} (hg : UniformContinuous g) (h : TendstoUniformly F f p) :
    TendstoUniformly (fun i => g ∘ F i) (g ∘ f) p := fun _u hu => h _ (hg hu)

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