English
If for every x∈s there exists t in nhdsWithin x s such that HasProdUniformlyOn f g {t}, then HasProdLocallyUniformlyOn f g s.
Русский
Если для каждого x∈s существует t из nhdsWithin x s such that HasProdUniformlyOn f g {t}, то HasProdLocallyUniformlyOn f g s.
LaTeX
$$$ (\forall x \in s, \exists t \in 𝓝[s] x, HasProdUniformlyOn f g { t }) \Rightarrow HasProdLocallyUniformlyOn f g s $$$
Lean4
/-- If every `x ∈ s` has a neighbourhood within `s` on which `b ↦ ∏' i, f i b` converges uniformly
to `g`, then the product converges locally uniformly on `s` to `g`. Note that this is not a
tautology, and the converse is only true if the domain is locally compact. -/
@[to_additive /-- If every `x ∈ s` has a neighbourhood within `s` on which `b ↦ ∑' i, f i b`
converges uniformly to `g`, then the sum converges locally uniformly. Note that this is not a
tautology, and the converse is only true if the domain is locally compact. -/
]
theorem hasProdLocallyUniformlyOn_of_of_forall_exists_nhds (h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, HasProdUniformlyOn f g { t }) :
HasProdLocallyUniformlyOn f g s :=
tendstoLocallyUniformlyOn_of_forall_exists_nhds <| by simpa [hasProdUniformlyOn_iff_tendstoUniformlyOn] using h
