English
Let f be a function between normed spaces and let s be a subset of its domain. If u is a neighborhood of x, then restricting to s ∩ u does not change the n-th iterated differential at x: iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x.
Русский
Пусть f: E → F, s ⊆ E, и пусть u является окрестностью точки x. Тогда n-ая повторная производная внутри множества не меняется при пересечении области: iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x.
LaTeX
$$$\forall n\ f:\,E\to F\,\forall s\subset E\,\forall x\in E\,\forall u\subset E,\ u\in 𝓝 x \ \Rightarrow\ iteratedFDerivWithin 𝕜 n f (s\cap u) x = iteratedFDerivWithin 𝕜 n f s x$$$
Lean4
/-- The iterated differential within a set `s` at a point `x` is not modified if one intersects
`s` with a neighborhood of `x`. -/
theorem iteratedFDerivWithin_inter {n : ℕ} (hu : u ∈ 𝓝 x) :
iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x :=
iteratedFDerivWithin_inter' (mem_nhdsWithin_of_mem_nhds hu)
