English
If f is a ContDiffBump with parameter c, then f is ContDiff of order n in all arguments, i.e. f ∈ ContDiff Real n for any n.
Русский
Если f — bump-функция с параметром c, то она гладка до любой степени по всем аргументам.
LaTeX
$$$\\forall {E X}: \\; [\\text{NormedAddCommGroup } E]\\ [\\text{NormedSpace } \\mathbb{R}E]\\ [\\text{NormedAddCommGroup } X]\\ [\\text{NormedSpace } \\mathbb{R}X]\\ [\\HasContDiffBump E] \\{c\\}, {f: ContDiffBump c}\\Rightarrow ContDiff Real (WithTop.some n) f.toFun$$$
Lean4
theorem _root_.ContDiff.contDiffBump {c g : X → E} {f : ∀ x, ContDiffBump (c x)} (hc : ContDiff ℝ n c)
(hr : ContDiff ℝ n fun x => (f x).rIn) (hR : ContDiff ℝ n fun x => (f x).rOut) (hg : ContDiff ℝ n g) :
ContDiff ℝ n fun x => f x (g x) := by
rw [contDiff_iff_contDiffAt] at *
exact fun x => (hc x).contDiffBump (hr x) (hR x) (hg x)
