iteratedDerivWithin_of_isOpen — Mathlib

English

If s is open, then iteratedDerivWithin n f s equals iteratedDeriv n f on s.

Русский

Если s открыто, то iteratedDerivWithin n f s совпадает с iteratedDeriv n f на s.

LaTeX

$$$\\IsOpen s \\Rightarrow Set.EqOn (iteratedDerivWithin n f s) (iteratedDeriv n f) s$$$

Lean4

theorem iteratedDerivWithin_of_isOpen (hs : IsOpen s) : Set.EqOn (iteratedDerivWithin n f s) (iteratedDeriv n f) s :=
  by
  intro x hx
  simp_rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_of_isOpen n hs hx]

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