English
If each g_i is continuous at tsupport of f_i and f_i is a partition of unity, then the finsum ∑ᶠ f_i g_i is continuous on X.
Русский
Если каждый g_i непрерывен на tsupport f_i, то сумма по finsum f_i g_i непрерывна на X.
LaTeX
$$$\text{ContinuousAdd } E \Rightarrow \text{Continuous}
(x \mapsto \sum^{\!\text{fin}} f_i(x)\,g_i(x))$$$
Lean4
/-- If `f` is a partition of unity on a set `s : Set X` and `g : ι → X → E` is a family of functions
such that each `g i` is continuous at every point of the topological support of `f i`, then the sum
`fun x ↦ ∑ᶠ i, f i x • g i x` is continuous on the whole space. -/
theorem continuous_finsum_smul [ContinuousAdd E] {g : ι → X → E}
(hg : ∀ (i), ∀ x ∈ tsupport (f i), ContinuousAt (g i) x) : Continuous fun x => ∑ᶠ i, f i x • g i x :=
(continuous_finsum fun i => f.continuous_smul (hg i)) <| f.locallyFinite.subset fun _ => support_smul_subset_left _ _
