differentiableAt_zero

Mathlib.Analysis.Calculus.FDeriv.Const

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

English

The zero map is differentiable at every point with derivative zero.

Русский

Нулевое отображение дифференцируемо в каждой точке с производной, равной нулю.

LaTeX

$$DifferentiableAt 𝕜 (0 : E → F) x$$

Lean4

@[simp, fun_prop]
theorem differentiableAt_zero (x : E) : DifferentiableAt 𝕜 (0 : E → F) x :=
  differentiableAt_const _

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

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

Разделы

Аффилиация

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