contDiff_neg

Mathlib.Analysis.Calculus.ContDiff.Operations

URI: https://scilib.ai/kg/mathlib#contDiff_neg

English

If f is C^n, then its negation -f is also C^n.

Русский

Если функция f принадлежит классу C^n, то и функция −f принадлежит этому классу.

LaTeX

$$$ ContDiff 𝕜 n f \implies ContDiff 𝕜 n (-f) $$$

Lean4

@[fun_prop]
theorem contDiff_neg : ContDiff 𝕜 n fun p : F => -p :=
  IsBoundedLinearMap.id.neg.contDiff

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

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

Разделы

Аффилиация

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