comp — Mathlib

English

If F f converge uniformly on p to f, then for any map g, the composed family F n ∘ g converges uniformly to f ∘ g on p.

Русский

Если F f сходятся равномерно по p к f, то для любого отображения g, F n ∘ g сходятся равномерно к f ∘ g по p.

LaTeX

$$TendstoUniformly F f p ⇒ TendstoUniformly (fun n => F n ∘ g) (f ∘ g) p$$

Lean4

/-- Composing on the right by a function preserves uniform convergence -/
theorem comp (h : TendstoUniformly F f p) (g : γ → α) : TendstoUniformly (fun n => F n ∘ g) (f ∘ g) p :=
  by
  rw [tendstoUniformly_iff_tendstoUniformlyOnFilter] at h ⊢
  simpa [principal_univ, comap_principal] using h.comp g

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