English
Let c,g : X → E, f : ∀ x, ContDiffBump (c x) be Cn in a neighborhood sense. If c, (f x).rIn, (f x).rOut, and g are all Cn at a point x, then the map x ↦ f x (g x) is Cn at x.
Русский
Пусть c, g: X → E, f: ∀ x, ContDiffBump (c x) и для некоторой точки x функция rIn, rOut зависят гладко; если c, (f x).rIn, (f x).rOut, g — гладко в окрестности точки, тогда x ↦ f x (g x) гладко до порядка n в этой точке.
LaTeX
$$$\\forall {E X} \\,[\\text{NormedAddCommGroup } E], [\\text{NormedSpace } \\mathbb{R}E], {c,g:X\\to E}, {f: \\forall x, ContDiffBump (c x)}, {x: X}, {n: \\mathbb{N}_{\\infty}}:\\ContDiffAt\\,\\mathbb{R}\\, n\\, c\\ x \\to \\ContDiffAt\\,\\mathbb{R}\\, n\\ (fun x => (f x).rIn)\\ x \\to \\ContDiffAt\\,\\mathbb{R}\\, n\\ (fun x => (f x).rOut)\\ x \\to \\ContDiffAt\\,\\mathbb{R}\\, n\\ g\\ x \\to \\ContDiffAt\\,\\mathbb{R}\\, n\\ (fun x => (f x).toFun (g x))\\ x$$
Lean4
/-- `ContDiffBump` is `𝒞ⁿ` in all its arguments. -/
protected nonrec theorem _root_.ContDiffAt.contDiffBump {c g : X → E} {f : ∀ x, ContDiffBump (c x)} {x : X}
(hc : ContDiffAt ℝ n c x) (hr : ContDiffAt ℝ n (fun x => (f x).rIn) x) (hR : ContDiffAt ℝ n (fun x => (f x).rOut) x)
(hg : ContDiffAt ℝ n g x) : ContDiffAt ℝ n (fun x => f x (g x)) x :=
hc.contDiffBump hr hR hg
