differentiableAt

Mathlib.Analysis.Calculus.Deriv.AffineMap

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

English

Let f be an affine map 𝕜 →ᵃ[𝕜] E. Then f is differentiable at every x ∈ 𝕜.

Русский

Пусть f — аффинное отображение 𝕜 →ᵃ[𝕜] E. Тогда функция f дифференцируема в любой точке x ∈ 𝕜.

LaTeX

$$$\\forall x\\in 𝕜:\\; \\text{DifferentiableAt}_{𝕜}(f,x).$$$

Lean4

protected theorem differentiableAt : DifferentiableAt 𝕜 f x :=
  f.hasDerivAt.differentiableAt

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

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

Разделы

Аффилиация

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