English
If f has compact support and is C^n, then its extension by 1 is C^n.
Русский
Если у f есть компактная поддержка и она C^n, то её продолжение единицей является C^n.
LaTeX
$$$\text{ContMDiff I I' n f} \Rightarrow \text{ContMDiff I I' n (Subtype.val.extend f 1)}$$$
Lean4
@[to_additive]
theorem extend_one [T2Space M] [One M'] {n : WithTop ℕ∞} {U : Opens M} {f : U → M'} (supp : HasCompactMulSupport f)
(diff : ContMDiff I I' n f) : ContMDiff I I' n (Subtype.val.extend f 1) := fun x ↦
by
refine contMDiff_of_mulTSupport (fun x h ↦ ?_) _
lift x to U using Subtype.coe_image_subset _ _ (supp.mulTSupport_extend_one_subset continuous_subtype_val h)
rw [← contMDiffAt_subtype_iff]
simp_rw [← comp_def]
rw [extend_comp Subtype.val_injective]
exact diff.contMDiffAt
