MultipliableLocallyUniformlyOn — Mathlib

English

Same as HasProdLocallyUniformlyOn: the property of local uniform convergence of the infinite product to g on s.

Русский

То же самое, что HasProdLocallyUniformlyOn: свойство локально-однородной сходимости бесконечного произведения к g на s.

LaTeX

$$$ HasProdLocallyUniformlyOn f g s \equiv TendstoLocallyUniformlyOn (\lambda I b. \prod_{i∈I} f i b) g atTop s $$$

Lean4

/-- `MultipliableLocallyUniformlyOn f s` means that the product `∏' i, f i b` converges locally
uniformly on `s` to something. -/
@[to_additive /-- `SummableLocallyUniformlyOn f s` means that `∑' i, f i b` converges locally
    uniformly on `s` to something. -/
    ]
def MultipliableLocallyUniformlyOn : Prop :=
  ∃ g, HasProdLocallyUniformlyOn f g s

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