sin — Mathlib

English

If f has ContDiffAt of order n at x on s, then sin(f) has ContDiffAt of order n at x on s.

Русский

Пусть f обладает ContDiffAt порядка n в точке x относительно множества s; тогда sin(f) имеет ту же ContDiffAt в точке x относительно s.

LaTeX

$$$\\\\text{ContDiffAt}_{\\\\mathbb{R}}^{n} f\,s\,x \\\\Rightarrow \\\\text{ContDiffAt}_{\\\\mathbb{R}}^{n} (\\\\sin \\circ f)\,s\,x$$$

Lean4

theorem sin {n} (hf : ContDiffAt ℝ n f x) : ContDiffAt ℝ n (fun x => Real.sin (f x)) x :=
  Real.contDiff_sin.contDiffAt.comp x hf

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