English
A general lemma about applying a constant continuous linear map to a function and differentiating within a set.
Русский
Общее лемма о применении константного непрерывного линейного отображения к функции и взятии производной внутри множества.
LaTeX
$$$\operatorname{ContDiffWithinAt}_{\mathbb{K}}\ n\ (f x)\;\text{...}$$$
Lean4
/-- `x ↦ fderivWithin 𝕜 (f x) t (g x) (k x)` is smooth at a point within a set. -/
theorem fderivWithin_apply {f : E → F → G} {g k : E → F} {t : Set F}
(hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (s ×ˢ t) (x₀, g x₀)) (hg : ContDiffWithinAt 𝕜 m g s x₀)
(hk : ContDiffWithinAt 𝕜 m k s x₀) (ht : UniqueDiffOn 𝕜 t) (hmn : m + 1 ≤ n) (hx₀ : x₀ ∈ s) (hst : s ⊆ g ⁻¹' t) :
ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) t (g x) (k x)) s x₀ :=
(contDiff_fst.clm_apply contDiff_snd).contDiffAt.comp_contDiffWithinAt x₀
((hf.fderivWithin hg ht hmn hx₀ hst).prodMk hk)
