hasDerivAt_lineMap

Mathlib.Analysis.Calculus.Deriv.AffineMap

URI: https://scilib.ai/kg/mathlib#AffineMap.hasDerivAt_lineMap

English

The lineMap between a and b has derivative b − a at x; i.e., HasDerivAt(lineMap a b) (b - a) x.

Русский

Линейная карта по точкам a и b имеет производную b−a в точке x.

LaTeX

$$$\\text{HasDerivAt}_{𝕜}(\\text{lineMap }a\\,b)\\ (b-a)\\ x.$$$

Lean4

theorem hasDerivAt_lineMap : HasDerivAt (lineMap a b) (b - a) x :=
  hasStrictDerivAt_lineMap.hasDerivAt

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

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

Разделы

Аффилиация

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