hasProdUniformlyOn — Mathlib

English

If h is MultipliableUniformlyOn f 𝔖, then there exists g such that HasProdUniformlyOn f g 𝔖.

Русский

Если h = MultipliableUniformlyOn f 𝔖, значит существует g, такое что HasProdUniformlyOn f g 𝔖.

LaTeX

$$$ [T2Space α]\ (h : MultipliableUniformlyOn f 𝔖) : HasProdUniformlyOn f (\prod' i, f i ·) 𝔖 $$$

Lean4

@[to_additive]
theorem hasProdUniformlyOn [T2Space α] (h : MultipliableUniformlyOn f 𝔖) : HasProdUniformlyOn f (∏' i, f i ·) 𝔖 :=
  by
  obtain ⟨g, hg⟩ := h.exists
  simp only [hasProdUniformlyOn_iff_tendstoUniformlyOn]
  intro s hs
  exact (hasProdUniformlyOn_iff_tendstoUniformlyOn.mp hg s hs).congr_right (hg.tprod_eqOn hs).symm

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