lineDifferentiableAt

Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap

URI: https://scilib.ai/kg/mathlib#QuadraticMap.lineDifferentiableAt

English

A quadratic map f is differentiable along the line at any pair (a, b).

Русский

Квадратичное отображение f дифференцируемо вдоль прямой для любой пары (a, b).

LaTeX

$$$ LineDifferentiableAt 𝕜 f a b$$$

Lean4

theorem lineDifferentiableAt (f : QuadraticMap 𝕜 E F) (a b : E) : LineDifferentiableAt 𝕜 f a b :=
  (f.hasLineDerivAt a b).lineDifferentiableAt

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

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

Разделы

Аффилиация

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