English
If M' is a subsingleton, any f: M → M' is ContMDiff.
Русский
Если M' подмножество единично, любая функция f: M → M' является ContMDiff.
LaTeX
$$$[Subsingleton M']\Rightarrow ContMDiff I I' n f$$$
Lean4
/-- Given two `C^n` functions `f` and `g` which coincide locally around the frontier of a set `s`,
then the piecewise function defined using `f` on `s` and `g` elsewhere is `C^n`. -/
theorem piecewise {f g : M → M'} {s : Set M} [DecidablePred (· ∈ s)] (hf : ContMDiff I I' n f) (hg : ContMDiff I I' n g)
(hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g) : ContMDiff I I' n (piecewise s f g) :=
by
intro x
by_cases hx : x ∈ interior s
· apply (hf x).congr_of_eventuallyEq
filter_upwards [isOpen_interior.mem_nhds hx] with y hy
rw [piecewise_eq_of_mem]
apply interior_subset hy
by_cases h'x : x ∈ closure s
· have : x ∈ frontier s := ⟨h'x, hx⟩
apply (hf x).congr_of_eventuallyEq
filter_upwards [hfg x this] with y hy
simp [Set.piecewise, hy]
· apply (hg x).congr_of_eventuallyEq
filter_upwards [isClosed_closure.isOpen_compl.mem_nhds h'x] with y hy
rw [piecewise_eq_of_notMem]
contrapose! hy
simpa using subset_closure hy
