comp — Mathlib

English

If F is locally uniform and g is continuous, then the composed map is locally uniform.

Русский

Если F локально равномерна и g непрерывна, то композиция локально равномерна.

LaTeX

$$$$\text{TendstoLocallyUniformly}(F,f,p)\Rightarrow \text{TendstoLocallyUniformly}((\lambda n, x \mapsto F_n(g(x))), (f\circ g), p).$$$$

Lean4

theorem comp [TopologicalSpace γ] (h : TendstoLocallyUniformly F f p) (g : γ → α) (cg : Continuous g) :
    TendstoLocallyUniformly (fun n => F n ∘ g) (f ∘ g) p :=
  by
  rw [← tendstoLocallyUniformlyOn_univ] at h ⊢
  rw [← continuousOn_univ] at cg
  exact h.comp _ (mapsTo_univ _ _) cg

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