English
The map x ↦ fderivWithin 𝕜 (f x) t (g x) is ContDiffWithinAt on s at x₀, under appropriate hypotheses.
Русский
Отображение x ↦ fderivWithin 𝕜 (f x) t (g x) непрерывно дифференцируемо внутри s в x₀ при определённых предположениях.
LaTeX
$$$\operatorname{ContDiffWithinAt}_{\mathbb{K}}\ m\ (\lambda x. fderivWithin\ 𝕜 (f x) t (g x))\ s\ x_0$$$
Lean4
/-- A special case of `ContDiffWithinAt.fderivWithin''` where we require that `s ⊆ g⁻¹(t)`. -/
theorem fderivWithin' {f : E → F → G} {g : E → F} {t : Set F}
(hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)) (hg : ContDiffWithinAt 𝕜 m g s x₀)
(ht : ∀ᶠ x in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)) (hmn : m + 1 ≤ n) (hst : s ⊆ g ⁻¹' t) :
ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) t (g x)) s x₀ :=
hf.fderivWithin'' hg ht hmn <| mem_of_superset self_mem_nhdsWithin <| image_subset_iff.mpr hst
