English
Same as above for ContMDiffOn with finite index set.
Русский
То же самое для ContMDiffOn с конечной индексной совокупностью.
LaTeX
$$ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s.sum fun i => t i x)) u$$
Lean4
/-- The scalar product `ψ • s` of a `C^k` function `ψ : M → 𝕜` and a section `s` of a vector
bundle `V → M` is `C^k` once `s` is `C^k` on an open set containing `tsupport ψ`.
This is a vector bundle analogue of `contMDiff_of_tsupport`. -/
theorem smul_section_of_tsupport {s : Π (x : M), V x} {ψ : M → 𝕜} (hψ : ContMDiffOn I 𝓘(𝕜) n ψ u) (ht : IsOpen u)
(ht' : tsupport ψ ⊆ u) (hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) u) :
ContMDiff I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (ψ x • s x)) :=
by
apply
contMDiff_of_contMDiffOn_union_of_isOpen (hψ.smul_section hs) ?_ ?_ ht (isOpen_compl_iff.mpr <| isClosed_tsupport ψ)
· apply ((contMDiff_zeroSection _ _).contMDiffOn (s := (tsupport ψ)ᶜ)).congr
intro y hy
simp [image_eq_zero_of_notMem_tsupport hy, zeroSection]
· exact Set.compl_subset_iff_union.mp <| Set.compl_subset_compl.mpr ht'
