English
If g_i is continuous at every point of tsupport of f_i, then the product x ↦ f_i(x)g_i(x) is continuous on X.
Русский
Если g_i непрерывна на tsupport f_i, то функция x ↦ f_i(x) g_i(x) непрерывна на X.
LaTeX
$$$\forall i,\forall x\in tsupport(f_i),\ ContinuousAt\ g_i(x) \Rightarrow \text{Continuous}(x\mapsto f_i(x)g_i(x))$$$
Lean4
/-- If `f` is a partition of unity on `s : Set X` and `g : X → E` is continuous at every point of
the topological support of some `f i`, then `fun x ↦ f i x • g x` is continuous on the whole space.
-/
theorem continuous_smul {g : X → E} {i : ι} (hg : ∀ x ∈ tsupport (f i), ContinuousAt g x) :
Continuous fun x => f i x • g x :=
continuous_of_tsupport fun x hx => ((f i).continuousAt x).smul <| hg x <| tsupport_smul_subset_left _ _ hx
