comp_tendstoUniformlyOn_eventually

English

If hF defines uniform convergence on a subset t of α and g is uniformly continuous on s, then TendstoUniformlyOn F f p t implies TendstoUniformlyOn (λ i x, g(F i x)) (g∘f) p t.

Русский

Если сходится равномерно на подмножестве t и g равномерно непрерывна на s, то сходимость сохраняется на t.

LaTeX

$$$\\text{TendstoUniformlyOn } F f p t \\Rightarrow \\text{TendstoUniformlyOn } (i, x \\mapsto g(F i x)) (x \\mapsto g(f x)) p t$$$

Lean4

theorem comp_tendstoUniformlyOn_eventually {t : Set α} (hF : ∀ᶠ i in p, ∀ x ∈ t, F i x ∈ s) (hf : ∀ x ∈ t, f x ∈ s)
    {g : β → γ} (hg : UniformContinuousOn g s) (h : TendstoUniformlyOn F f p t) :
    TendstoUniformlyOn (fun i x ↦ g (F i x)) (fun x => g (f x)) p t :=
  by
  rw [tendstoUniformlyOn_iff_restrict]
  apply
    UniformContinuousOn.comp_tendstoUniformly_eventually (by simpa using hF) (by simpa using hf) hg
      (tendstoUniformlyOn_iff_restrict.mp h)

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