English
If u is open and x ∈ u, intersecting s with u does not alter the iterated derivative within: iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x.
Русский
Если u открыто и x ∈ u, то пересечение s с u не меняет итеративную производную внутри: iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x.
LaTeX
$$$\forall n\ f:\,E\to F,\ s,t\subset E,\ x\in E,\ u\subset E,\ IsOpen\ u \to x\in u \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 an open set containing `x`. -/
theorem iteratedFDerivWithin_inter_open {n : ℕ} (hu : IsOpen u) (hx : x ∈ u) :
iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x :=
iteratedFDerivWithin_inter (hu.mem_nhds hx)
