fderiv_of_notMem_tsupport

Mathlib.Analysis.Calculus.FDeriv.Const

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

English

If x ∉ tsupport f, then the derivative fderiv 𝕜 f x equals 0.

Русский

Если x не принадлежит tsupport функции f, то производная f равна нулю.

LaTeX

$$$\exists x: (x \notin tsupport(f)) \Rightarrow fderiv 𝕜 f x = 0$$$

Lean4

theorem fderiv_of_notMem_tsupport (h : x ∉ tsupport f) : fderiv 𝕜 f x = 0 :=
  (HasFDerivAt.of_notMem_tsupport 𝕜 h).fderiv

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

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

Разделы

Аффилиация

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