iteratedDerivWithin_cosh_Ioo — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem iteratedDerivWithin_cosh_Ioo (n : ℕ) {a b x : ℝ} (hx : x ∈ Ioo a b) :
    iteratedDerivWithin n cosh (Ioo a b) x = iteratedDeriv n cosh x :=
  iteratedDerivWithin_eq_iteratedDeriv (uniqueDiffOn_Ioo a b) contDiff_cosh.contDiffAt hx

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