DifferentiableAt

Mathlib.Analysis.Calculus.FDeriv.Defs

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

← 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

/-- A function `f` is differentiable at a point `x` if it admits a derivative there (possibly
non-unique). -/
@[fun_prop]
def DifferentiableAt (f : E → F) (x : E) :=
  ∃ f' : E →L[𝕜] F, HasFDerivAt f f' x

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

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

Разделы

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

Аффилиация

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