MultipliableUniformlyOn — Mathlib

English

If f is MultipliableUniformlyOn on 𝔖, then there exists a function g with HasProdUniformlyOn f g 𝔖.

Русский

Если f имеет MultipliableUniformlyOn на 𝔖, то существует функция g такая, что HasProdUniformlyOn f g 𝔖.

LaTeX

$$$\\exists g\\; HasProdUniformlyOn\ufeff f\\ g\\ 𝔖$$$

Lean4

/-- `MultipliableUniformlyOn f 𝔖` means that there is some infinite product to which
`f` converges uniformly on every `s ∈ 𝔖`. Use `fun x ↦ ∏' i, f i x` to get the product function. -/
@[to_additive /-- `SummableUniformlyOn f s` means that there is some infinite sum to
    which `f` converges uniformly on every `s ∈ 𝔖`. Use fun x ↦ ∑' i, f i x to get the sum function. -/
    ]
def MultipliableUniformlyOn : Prop :=
  Multipliable (fun i ↦ UniformOnFun.ofFun 𝔖 (f i))

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