sinh — Mathlib

English

If f is ContDiffWithinAt ℝ n on s at x, then sinh ∘ f is ContDiffWithinAt ℝ n on s at x.

Русский

Если f имеет ContDiffWithinAt ℝ n на подмножестве s в точке x, то sinh ∘ f имеет ContDiffWithinAt ℝ n на s в точке x.

LaTeX

$$$\operatorname{ContDiffWithinAt}_{\mathbb{R}}^{n}(f, s, x) \Rightarrow \operatorname{ContDiffWithinAt}_{\mathbb{R}}^{n}( \sinh \circ f, s, x ).$$$

Lean4

theorem sinh {n} (hf : ContDiffWithinAt ℝ n f s x) : ContDiffWithinAt ℝ n (fun x => Real.sinh (f x)) s x :=
  Real.contDiff_sinh.contDiffAt.comp_contDiffWithinAt x hf

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