iteratedFDerivWithin_inter' — Mathlib

English

If two sets agree on nhds x, then their iterated derivatives at x agree for all n.

Русский

Если множества совпадают в окрестности x, их производные совпадают в x для всех n.

LaTeX

$$$\forall h: (nhds x).EventuallyEq s t,\forall n, (iteratedFDerivWithin 𝕜 n f s x) = (iteratedFDerivWithin 𝕜 n f t 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` within `s`. -/
theorem iteratedFDerivWithin_inter' {n : ℕ} (hu : u ∈ 𝓝[s] x) :
    iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x :=
  iteratedFDerivWithin_congr_set (nhdsWithin_eq_iff_eventuallyEq.1 <| nhdsWithin_inter_of_mem' hu) _

Похожие утверждения