hasProdLocallyUniformlyOn — Mathlib

English

If h is MultipliableLocallyUniformlyOn f s, then HasProdLocallyUniformlyOn f (∏' i, f i ·) s.

Русский

Если h = MultipliableLocallyUniformlyOn f s, то HasProdLocallyUniformlyOn f (∏' i, f i ·) s.

LaTeX

$$$ [T2Space α] (h : MultipliableLocallyUniformlyOn f s) : HasProdLocallyUniformlyOn f (\prod' i, f i \cdot) s $$$

Lean4

@[to_additive]
theorem hasProdLocallyUniformlyOn [T2Space α] (h : MultipliableLocallyUniformlyOn f s) :
    HasProdLocallyUniformlyOn f (∏' i, f i ·) s :=
  match h with
  | ⟨_, hg⟩ => hg.congr_right fun _ hb ↦ (hg.hasProd hb).tprod_eq.symm

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