iteratedDerivWithin_sin_Icc — Mathlib

English

For every n and for a<b, if x belongs to the closed interval Icc(a,b), then the iterated deriv within equals the ordinary iterated deriv at x.

Русский

Для каждого n и a<b, если x ∈ Icc(a,b), то iteratedDerivWithin n sin (Icc a b) x = iteratedDeriv n sin x.

LaTeX

$$$\\\\forall n \\in \\mathbb{N},\\\\; \\\\forall a < b,\\\\; \\forall x \\in Icc(a,b): \\\\ iteratedDerivWithin n \\ sin (Icc(a,b)) x = \\\\ iteratedDeriv n \\ sin x$$$

Lean4

@[simp]
theorem iteratedDerivWithin_sin_Icc (n : ℕ) {a b : ℝ} (h : a < b) {x : ℝ} (hx : x ∈ Icc a b) :
    iteratedDerivWithin n sin (Icc a b) x = iteratedDeriv n sin x :=
  iteratedDerivWithin_eq_iteratedDeriv (uniqueDiffOn_Icc h) contDiff_sin.contDiffAt hx

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