English
Special case where s ⊆ g^{-1}(t) ensures fderivWithin is ContDiffWithinAt on s.
Русский
Особый случай, когда s ⊆ g^{−1}(t), обеспечивает fderivWithin гладкость внутри s.
LaTeX
$$$\operatorname{ContDiffWithinAt}_{\mathbb{K}}\ m (\mathrm{fderivWithin}\ 𝕜 (f x) t (g x))\ s x_0$$$
Lean4
/-- A special case of `ContDiffWithinAt.fderivWithin'` where we require that `x₀ ∈ s` and there
are unique derivatives everywhere within `t`. -/
protected theorem fderivWithin {f : E → F → G} {g : E → F} {t : Set F}
(hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (s ×ˢ t) (x₀, g x₀)) (hg : ContDiffWithinAt 𝕜 m g 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)) s x₀ :=
by
rw [← insert_eq_self.mpr hx₀] at hf
refine hf.fderivWithin' hg ?_ hmn hst
rw [insert_eq_self.mpr hx₀]
exact eventually_of_mem self_mem_nhdsWithin fun x hx => ht _ (hst hx)
