csin

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

URI: https://scilib.ai/kg/mathlib#ContDiff.csin

English

If h is ContDiff, then sin ∘ h is ContDiff with the same order.

Русский

Если h ∈ ContDiff, то sin ∘ h имеет такую же ContDiff, как и h.

LaTeX

$$$\\text{ContDiff}(\\mathbb{C}, n, f) \\Rightarrow \\text{ContDiff}(\\mathbb{C}, n, \\sin\\circ f).$$$

Lean4

theorem csin {n} (h : ContDiff ℂ n f) : ContDiff ℂ n fun x => Complex.sin (f x) :=
  Complex.contDiff_sin.comp h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru