sin — Mathlib

English

If f is ContDiffOn Real n f s, then sin(f) is ContDiffOn Real n f s.

Русский

Если f имеет ContDiffOn Real n на s, то sin(f) тоже имеет ContDiffOn Real n на s.

LaTeX

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

Lean4

theorem sin {n} (hf : ContDiffOn ℝ n f s) : ContDiffOn ℝ n (fun x => Real.sin (f x)) s :=
  Real.contDiff_sin.comp_contDiffOn hf

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