English
If g is smooth on the chart source, then f · g is smooth on the manifold.
Русский
Если g гладкая на областиchartAt c, то f·g гладкая на многообразии.
LaTeX
$$ContMDiffOn I 𝓘(ℝ, G) ∞ g (chartAt H c).source → ContMDiff I 𝓘(ℝ, G) ∞ (fun x => f x • g x)$$
Lean4
/-- If `f : SmoothBumpFunction I c` is a smooth bump function and `g : M → G` is a function smooth
on the source of the chart at `c`, then `f • g` is smooth on the whole manifold. -/
theorem contMDiff_smul {G} [NormedAddCommGroup G] [NormedSpace ℝ G] {g : M → G}
(hg : ContMDiffOn I 𝓘(ℝ, G) ∞ g (chartAt H c).source) : ContMDiff I 𝓘(ℝ, G) ∞ fun x => f x • g x :=
by
refine
contMDiff_of_tsupport fun x hx =>
?_
-- Porting note: was a more readable `calc`
-- calc
-- x ∈ tsupport fun x => f x • g x := hx
-- _ ⊆ tsupport f := tsupport_smul_subset_left _ _
-- _ ⊆ (chart_at _ c).source := f.tsupport_subset_chartAt_source
have : x ∈ (chartAt H c).source := f.tsupport_subset_chartAt_source <| tsupport_smul_subset_left _ _ hx
exact f.contMDiffAt.smul ((hg _ this).contMDiffAt <| (chartAt _ _).open_source.mem_nhds this)
