sinh — Mathlib

English

If DifferentiableWithinAt Real f s x, then DifferentiableWithinAt Real (sin h (f x)) s x.

Русский

Если f дифференцируема внутри s в точке x, то sinh(f(x)) дифференцируема внутри s в точке x.

LaTeX

$$DifferentiableWithinAt Real f s x → DifferentiableWithinAt Real (fun x => Real.sinh (f x)) s x$$

Lean4

theorem sinh (hf : DifferentiableWithinAt ℝ f s x) : DifferentiableWithinAt ℝ (fun x => Real.sinh (f x)) s x :=
  hf.hasFDerivWithinAt.sinh.differentiableWithinAt

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