iteratedDerivWithin_sinh_Icc — Mathlib

English

Let n be a nonnegative integer and a < b. For every x ∈ [a,b], the nth iterated derivative of sinh on [a,b] at x equals the ordinary nth derivative of sinh at x.

Русский

Пусть n — неотрицательное целое число и a < b. Для каждого x ∈ [a,b] n-я итеративная производная sinh на [a,b] в точке x совпадает с обычной n-й производной sinh в x.

LaTeX

$$$D^{n}\\bigl(\\sinh\\bigr)\\big|_{[a,b]}(x) = D^{n}\\bigl(\\sinh\\bigr)(x),\\quad a

Lean4

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

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