hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn

English

HasProdLocallyUniformlyOn f g s is equivalent to TendstoLocallyUniformlyOn of the corresponding finite products on atTop on s.

Русский

HasProdLocallyUniformlyOn f g s эквивалентно TendstoLocallyUniformlyOn соответствующих конечных произведений на atTop по s.

LaTeX

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

Lean4

@[to_additive]
theorem hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn :
    HasProdLocallyUniformlyOn f g s ↔ TendstoLocallyUniformlyOn (fun I b ↦ ∏ i ∈ I, f i b) g atTop s :=
  Iff.rfl

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