comp_tendstoUniformlyOn — Mathlib

English

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

Русский

Если g равномерно непрерывна и существует TendstoUniformlyOn F f p s, то TendstoUniformlyOn (g ∘ F) (g ∘ f) p s выполняется.

LaTeX

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

Lean4

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

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