English
If x ∉ mulTSupport f, then ContMDiffAt I I' n f x holds for all n.
Русский
Если x ∉ mulTSupport(f), то ContMDiffAt I I' n f x выполняется для всех n.
LaTeX
$$$Not( x \in mulTSupport(f) ) \Rightarrow ContMDiffAt_I_I'_n f x$$
Lean4
/-- `f` is continuously differentiable if it is cont. differentiable at
each `x ∈ mulTSupport f`. -/
@[to_additive /-- `f` is continuously differentiable if it is continuously
differentiable at each `x ∈ tsupport f`. See also `contMDiff_section_of_tsupport`
for a similar result for sections of vector bundles. -/
]
theorem contMDiff_of_mulTSupport [One M'] {f : M → M'} (hf : ∀ x ∈ mulTSupport f, ContMDiffAt I I' n f x) :
ContMDiff I I' n f := by
intro x
by_cases hx : x ∈ mulTSupport f
· exact hf x hx
· exact ContMDiffAt.congr_of_eventuallyEq contMDiffAt_const (notMem_mulTSupport_iff_eventuallyEq.1 hx)
