lineDifferentiableAt_zero

Mathlib.Analysis.Calculus.LineDeriv.Basic

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

English

Line differentiability at a point with zero direction is guaranteed by a baseline lemma.

Русский

Линейная дифференцируемость в точке при нулевом направлении обеспечена базовым леммой.

LaTeX

$$$LineDifferentiableAt_{\\mathbb{K}}(f,x,0) \\,\\text{ holds by baseline }$$

Lean4

theorem lineDifferentiableAt_zero : LineDifferentiableAt 𝕜 f x 0 :=
  hasLineDerivAt_zero.lineDifferentiableAt

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

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

Разделы

Аффилиация

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