comp_tendstoUniformlyOnFilter — Mathlib

English

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

Русский

Если g равномерно непрерывна и существует TendstoUniformlyOnFilter F f p p', то также существует TendstoUniformlyOnFilter (g ∘ F) (g ∘ f) p p'.

LaTeX

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

Lean4

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

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