tendstoUniformlyOn — Mathlib

English

If F f converge uniformly on p to s, and g maps γ to α, then the composed family F n ∘ g converges uniformly to f ∘ g on the preimage of s under g, i.e., g^{-1}(s).

Русский

Если F f сходятся равномерно по p к f, то F n ∘ g сходится равномерно к f ∘ g на прообразе s по g, то есть на g^{-1}(s).

LaTeX

$$TendstoUniformlyOn F f p s ⇒ TendstoUniformlyOn (fun n => F n ∘ g) (f ∘ g) p (g^{-1} s)$$

Lean4

protected theorem tendstoUniformlyOn (h : TendstoUniformly F f p) : TendstoUniformlyOn F f p s :=
  (tendstoUniformlyOn_univ.2 h).mono (subset_univ s)

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