rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_of_isOpen _ hs hx]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
f : 𝕜 → F
n : ℕ
hs : IsOpen s
x : 𝕜
hx : x ∈ s
⊢ iteratedDerivWithin n f s x = iteratedDeriv n f x
no goals