sub

Mathlib.Analysis.Calculus.FDeriv.Add

URI: https://scilib.ai/kg/mathlib#DifferentiableWithinAt.sub

← MathLib Explorer

English

For any f, f′(−f) = − f′(f).

Русский

Для любой функции f: f′(−f) = − f′(f).

LaTeX

$$fderiv 𝕜 (−f) x = − fderiv 𝕜 f x$$

Lean4

@[fun_prop]
theorem sub (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :
    DifferentiableWithinAt 𝕜 (f - g) s x :=
  hf.fun_sub hg

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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