iteratedFDerivWithin — Mathlib

English

If two functions agree on a set s, their iterated derivatives within s agree on s.

Русский

Если две функции совпадают на множестве s, их итеративные производные внутри s совпадают на s.

LaTeX

$$$\forall hs: EqOn f₁ f s,\forall n,\forall x\in s, iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 n f s x$$$

Lean4

/-- If two functions coincide on a set `s`, then their iterated differentials within this set
coincide. See also `Filter.EventuallyEq.iteratedFDerivWithin_eq` and
`Filter.EventuallyEq.iteratedFDerivWithin`. -/
protected theorem iteratedFDerivWithin (hs : EqOn f₁ f s) (n : ℕ) :
    EqOn (iteratedFDerivWithin 𝕜 n f₁ s) (iteratedFDerivWithin 𝕜 n f s) s := fun _x hx =>
  iteratedFDerivWithin_congr hs hx n

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