arsinh — Mathlib

English

If f is ContDiffAt at a, then arsinh ∘ f is ContDiffAt at a of the same order.

Русский

Если f имеет непрерывную дифференцируемость заданной степени в точке a, то arsinh(f(x)) имеет ту же ContDiffAt в точке a.

LaTeX

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

Lean4

@[fun_prop]
theorem arsinh (h : ContDiffAt ℝ n f a) : ContDiffAt ℝ n (fun x => arsinh (f x)) a :=
  contDiff_arsinh.contDiffAt.comp a h

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