multipliableLocallyUniformlyOn_one_add

English

With a single open K and summable u, the product ∏' i (1+f_i x) converges uniformly on K given continuity on K and eventual bounds.

Русский

Для единого открытого множества K и суммируемой u произведение ∏' i (1+f_i x) сходится равномерно на K при условии непрерывности на K и локально ограниченных f_i.

LaTeX

$$$HasProdUniformlyOn\\ (\\lambda i x, 1+f_i(x))\\ (\\lambda x, ∏' i, (1+f_i(x)))\\ {K}$$$

Lean4

theorem multipliableLocallyUniformlyOn_one_add (hK : IsOpen K) (hu : Summable u)
    (h : ∀ᶠ i in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) (hcts : ∀ i, ContinuousOn (f i) K) :
    MultipliableLocallyUniformlyOn (fun i x ↦ 1 + f i x) K :=
  ⟨_, hasProdLocallyUniformlyOn_one_add hK hu h hcts⟩

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