differentiableOn_singleton

Mathlib.Analysis.Calculus.FDeriv.Const

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

English

A function is differentiable on a singleton set {x}.

Русский

Функция дифференцируема на множестве вида {x}.

LaTeX

$$$\mathrm{DifferentiableOn}_{\mathbb{k}} f \{x\}$$$

Lean4

@[fun_prop]
theorem differentiableOn_singleton : DifferentiableOn 𝕜 f { x } :=
  forall_eq.2 (hasFDerivWithinAt_singleton f x).differentiableWithinAt

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

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

Разделы

Аффилиация

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