ccosh — Mathlib

English

If f is differentiable within s at x, then cosh(f) is differentiable within s at x.

Русский

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

LaTeX

$$$$ \text{DifferentiableWithinAt}_{\mathbb{C}}(f,s,x) \Rightarrow \text{DifferentiableWithinAt}_{\mathbb{C}}(\cosh(f),s,x). $$$$

Lean4

theorem ccosh (hf : DifferentiableWithinAt ℂ f s x) : DifferentiableWithinAt ℂ (fun x => Complex.cosh (f x)) s x :=
  hf.hasFDerivWithinAt.ccosh.differentiableWithinAt

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