English
Let f be differentiable within a set s at x and assume x is a unique point within s. Then the derivative within s of the composition x ↦ sinh(f(x)) is cosh(f(x)) times the derivative within s of f at x.
Русский
Пусть f дифференцируема внутри множества s в точке x и в этой точке выполняется уникальность точки внутри s. Тогда fderivWithinℝ( Real.sinh ∘ f ) s x = cosh(f(x)) · fderivWithinℝ f s x.
LaTeX
$$$\forall E\ [\text{NormedAddCommGroup } E]\ [\text{NormedSpace } \mathbb{R} E],\ {f: E \to \mathbb{R}},\ {s: \text{Set } E},\ (\text{DifferentiableWithinAt } \mathbb{R} f\ s\ x)\ (\text{UniqueDiffWithinAt } \mathbb{R} s\ x) \Rightarrow \\ fderivWithin\mathbb{R}(\lambda x: \sinh(f x))\ s x = \cosh(f x) \cdot fderivWithin\mathbb{R} f s x.$$$
Lean4
theorem fderivWithin_sinh (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
fderivWithin ℝ (fun x => Real.sinh (f x)) s x = Real.cosh (f x) • fderivWithin ℝ f s x :=
hf.hasFDerivWithinAt.sinh.fderivWithin hxs
