English
If s ⊆ t and s,t are uniquely differentiable, and f is C^n on t, then iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x for x ∈ s.
Русский
Если s ⊆ t и s,t обладают UniqueDiffOn, и f ∈ ContDiffOn 𝕜 n f t, то iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x при x ∈ s.
LaTeX
$$$s\\subseteq t \\rightarrow UniqueDiffOn\\ 𝕜 s \\rightarrow UniqueDiffOn\\ 𝕜 t \\rightarrow ContDiffOn\\ 𝕜 n.f t \\rightarrow x\\in s\\rightarrow iteratedFDerivWithin\\ 𝕜 n f\\ s\\ x = iteratedFDerivWithin\\ 𝕜 n f\\ t\\ x$$$
Lean4
theorem iteratedFDerivWithin_subset {n : ℕ} (st : s ⊆ t) (hs : UniqueDiffOn 𝕜 s) (ht : UniqueDiffOn 𝕜 t)
(h : ContDiffOn 𝕜 n f t) (hx : x ∈ s) : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x :=
(((h.ftaylorSeriesWithin ht).mono st).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl hs hx).symm
