English
Let E be a real normed vector space and f: E → ℝ be differentiable. Then the function x ↦ sinh(f(x)) is differentiable on E, and its derivative at x is cosh(f(x)) times the derivative of f at x; i.e., D(sinh(f))(x) = cosh(f(x)) · Df(x).
Русский
Пусть E — нормированное векторное пространство над ℝ, и f: E → ℝ дифференцируема. Тогда функция x ↦ sinh(f(x)) дифференцируема на E, а её производная в точке x равна cosh(f(x)) умножить на производную f в x: D(sinh(f))(x) = cosh(f(x)) · Df(x).
LaTeX
$$$\forall E\ [\text{NormedAddCommGroup } E]\ [\text{NormedSpace } \mathbb{R} E],\ {f: E \to \mathbb{R}},\ (\text{Differentiable}_{\mathbb{R}} f) \Rightarrow \Big( \text{Differentiable}_{\mathbb{R}}\big( \lambda x: \sinh(f(x))\big) \wedge \forall x,\; D(\sinh\circ f)(x) = \cosh(f(x)) \cdot Df(x) \Big).$$$
Lean4
@[simp, fun_prop]
theorem sinh (hc : Differentiable ℝ f) : Differentiable ℝ fun x => Real.sinh (f x) := fun x => (hc x).sinh
