arsinh — Mathlib

English

If f is differentiable within s at a, then arsinh ∘ f is differentiable within s at a.

Русский

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

LaTeX

$$$\text{DifferentiableWithinAt } f\ s\ a \Rightarrow \text{DifferentiableWithinAt } (x \mapsto \operatorname{arsinh}(f(x)))\ s\ a$$$

Lean4

@[fun_prop]
theorem arsinh (h : DifferentiableWithinAt ℝ f s a) : DifferentiableWithinAt ℝ (fun x => arsinh (f x)) s a :=
  (differentiable_arsinh _).comp_differentiableWithinAt a h

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