English
If M' is a subsingleton, then ContMDiffWithinAt I I' n f s x holds for all s and x.
Русский
Если M' единично, то ContMDiffWithinAt I I' n f s x выполняется для всех s и x.
LaTeX
$$$[Subsingleton M']\Rightarrow ContMDiffWithinAt I I' n f s x$$$
Lean4
/-- Given two `C^n` functions `f` and `g` from `ℝ` to a real manifold which coincide locally
around a point `s`, then the piecewise function using `f` before `t` and `g` after is `C^n`. -/
theorem piecewise_Iic {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H]
{I : ModelWithCorners ℝ E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M] {f g : ℝ → M} {s : ℝ}
(hf : ContMDiff 𝓘(ℝ) I n f) (hg : ContMDiff 𝓘(ℝ) I n g) (hfg : f =ᶠ[𝓝 s] g) :
ContMDiff 𝓘(ℝ) I n (Set.piecewise (Iic s) f g) :=
hf.piecewise hg (by simpa using hfg)
