sin — Mathlib

English

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

Русский

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

LaTeX

$$$\\text{DifferentiableWithinAt }\\mathbb{R} f s x \\Rightarrow \\text{DifferentiableWithinAt }\\mathbb{R} (\\sin(f(x))) s x$$$

Lean4

theorem sin (hf : DifferentiableWithinAt ℝ f s x) : DifferentiableWithinAt ℝ (fun x => Real.sin (f x)) s x :=
  hf.hasFDerivWithinAt.sin.differentiableWithinAt

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