multipliableUniformlyOn — Mathlib

English

If a family f and a target g satisfy that the partial products ∏ i∈I f(i,·) converge uniformly to g on every set in 𝔖, then f is MultipliableUniformlyOn on 𝔖; i.e., there exists a function g such that HasProdUniformlyOn f g 𝔖.

Русский

Если семейство функций f и предел g удовлетворяют условию, что частичные произведения ∏ i∈I f(i,·) сходятся равномерно к g на каждой множестве из 𝔖, то f является MultipliableUniformlyOn на 𝔖; то есть существует функция g такая, что HasProdUniformlyOn f g 𝔖.

LaTeX

$$$ HasProdUniformlyOn\ f\ g\ 𝔖 \Rightarrow MultipliableUniformlyOn\ f\ 𝔖 $$$

Lean4

@[to_additive]
theorem multipliableUniformlyOn (h : HasProdUniformlyOn f g 𝔖) : MultipliableUniformlyOn f 𝔖 :=
  ⟨g, h⟩

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