English
If a TendstoUniformlyOnFilter F f p p' holds and g is a map, then composing on the left by g preserves uniform convergence on filters, i.e., TendstoUniformlyOnFilter (fun i => g ∘ F i) (g ∘ f) p p' holds.
Русский
Если существует сходимость равномерная по фильтру, сохраняемая под композицию слева через g, то остаётся сходимость равномерная.
LaTeX
$$hg : TendstoUniformlyOnFilter F f p p' ⇒ TendstoUniformlyOnFilter (fun i => g ∘ F i) (g ∘ f) p p'$$
Lean4
/-- Composing on the right by a function preserves uniform convergence on a filter -/
theorem comp (h : TendstoUniformlyOnFilter F f p p') (g : γ → α) :
TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (p'.comap g) :=
by
rw [tendstoUniformlyOnFilter_iff_tendsto] at h ⊢
exact h.comp (tendsto_id.prodMap tendsto_comap)
