of_notMem_tsupport

Mathlib.Analysis.Calculus.FDeriv.Const

URI: https://scilib.ai/kg/mathlib#HasFDerivAt.of_notMem_tsupport

English

If x is not in tsupport of f, then HasFDerivAt f (0 : E →L[𝕜] F) x holds.

Русский

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

LaTeX

$$$\text{If } x \notin tsupport(f) \; \Rightarrow \; \text{HasFDerivAt } f (0 : E \toL[𝕜] F) x$$$

Lean4

theorem of_notMem_tsupport (h : x ∉ tsupport f) : HasFDerivAt f (0 : E →L[𝕜] F) x :=
  (HasStrictFDerivAt.of_notMem_tsupport 𝕜 h).hasFDerivAt

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

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

Разделы

Аффилиация

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