comp — Mathlib

English

If F f converge uniformly on p to s, then composing on the right by g yields TendstoUniformlyOn (F ∘ g) (f ∘ g) p (preimage g s).

Русский

Если F f сходятся равномерно по p на s, то после композиции справа по g имеем сходность на предобразе s.

LaTeX

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

Lean4

/-- Composing on the right by a function preserves uniform convergence on a set -/
theorem comp (h : TendstoUniformlyOn F f p s) (g : γ → α) : TendstoUniformlyOn (fun n => F n ∘ g) (f ∘ g) p (g ⁻¹' s) :=
  by
  rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at h ⊢
  simpa [TendstoUniformlyOn, comap_principal] using TendstoUniformlyOnFilter.comp h g

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