English
If a partition of unity f is subordinate to open sets U and a family g with each g_i continuous on U_i, then the finite sum x ↦ ∑ᶠ i, f_i(x)·g_i(x) is continuous.
Русский
Если разбиение единиц f подчинено открытым множествам U и семейство функций g таково, что каждая g_i непрерывна на U_i, то сумма x ↦ ∑ᶠ i, f_i(x)·g_i(x) непрерывна.
LaTeX
$$$$\text{Continuous}\left( x \mapsto \sum_{i}^{\mathrm{Fin}} f_i(x)\, g_i(x) \right).$$$$
Lean4
/-- If `f` is a partition of unity that is subordinate to a family of open sets `U i` and
`g : ι → X → E` is a family of functions such that each `g i` is continuous on `U i`, then the sum
`fun x ↦ ∑ᶠ i, f i x • g i x` is a continuous function. -/
theorem continuous_finsum_smul [ContinuousAdd E] {U : ι → Set X} (ho : ∀ i, IsOpen (U i)) (hf : f.IsSubordinate U)
{g : ι → X → E} (hg : ∀ i, ContinuousOn (g i) (U i)) : Continuous fun x => ∑ᶠ i, f i x • g i x :=
f.continuous_finsum_smul fun i _ hx => (hg i).continuousAt <| (ho i).mem_nhds <| hf i hx
