hasStrictDerivAt_sinh — Mathlib

English

Near zero, sinh x is asymptotically equivalent to x; equivalently, sinh x ~ x as x → 0.

Русский

Поскольку x → 0, sinh x асимптотически эквивалентно x; sinh x ~ x при x → 0.

LaTeX

$$$\sinh z \sim z\quad (z \to 0)$$$

Lean4

/-- The complex hyperbolic sine function is everywhere strictly differentiable, with the derivative
`cosh x`. -/
theorem hasStrictDerivAt_sinh (x : ℂ) : HasStrictDerivAt sinh (cosh x) x :=
  by
  simp only [cosh, div_eq_mul_inv]
  convert ((hasStrictDerivAt_exp x).sub (hasStrictDerivAt_id x).fun_neg.cexp).mul_const (2 : ℂ)⁻¹ using 1
  rw [id, mul_neg_one, sub_eq_add_neg, neg_neg]

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