fderiv_apply

Mathlib.Analysis.Calculus.FDeriv.Const

URI: https://scilib.ai/kg/mathlib#HasCompactSupport.fderiv_apply

← MathLib Explorer

English

If x ∉ tsupport f, then HasFDerivAt f (0) x.

Русский

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

LaTeX

$$$x \notin tsupport(f) \Rightarrow \text{HasFDerivAt } f (0) x$$$

Lean4

protected theorem fderiv_apply (hf : HasCompactSupport f) (v : E) : HasCompactSupport (fderiv 𝕜 f · v) :=
  hf.fderiv 𝕜 |>.comp_left (g := fun L : E →L[𝕜] F ↦ L v) rfl

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

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

Разделы

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

Аффилиация

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