English
Alternative presentation: if every open neighborhood within s yields uniform convergence on a compact subset, then local uniform convergence on s holds.
Русский
Альтернативная формулировка: если для каждого открытого окрестности внутри s существует компактная подмножество, на котором сходится равномерно, тогда локальная равномерность на s выполняется.
LaTeX
$$$ \text{[...]} HasProdLocallyUniformlyOn f g s $$$
Lean4
/-- If every `x ∈ s` has a neighbourhood within `s` on which `b ↦ ∏' i, f i b` converges uniformly,
then the product converges locally uniformly on `s`. 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, 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 multipliableLocallyUniformlyOn_of_of_forall_exists_nhds [T2Space α]
(h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, MultipliableUniformlyOn f { t }) : MultipliableLocallyUniformlyOn f s :=
(hasProdLocallyUniformlyOn_of_of_forall_exists_nhds <| fun x hx ↦
match h x hx with
| ⟨t, ht, htr⟩ => ⟨t, ht, htr.hasProdUniformlyOn⟩).multipliableLocallyUniformlyOn
