iteratedFDerivWithin_insert — Mathlib

English

Inserting a point into the set does not change the iterated derivative at any y.

Русский

Вставка точки в множество не изменяет итеративную производную в любой y.

LaTeX

$$$\forall n,\ iterationFDerivWithin 𝕜 n f (insert x s) y = iteratedFDerivWithin 𝕜 n f s y$$$

Lean4

@[simp]
theorem iteratedFDerivWithin_insert {n y} :
    iteratedFDerivWithin 𝕜 n f (insert x s) y = iteratedFDerivWithin 𝕜 n f s y :=
  iteratedFDerivWithin_congr_set' (y := x) (eventually_mem_nhdsWithin.mono <| by intros; simp_all).set_eq _

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