differentiableAt

Mathlib.Analysis.Calculus.AddTorsor.AffineMap

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

English

For every x, the underlying function of a continuous affine map f: V →ᴬ[𝕜] W is differentiable at x.

Русский

Для любой точки x непрерывное афинное отображение f: V →ᴬ[𝕜] W дифференцируемо в точке x.

LaTeX

$$$ \operatorname{DifferentiableAt}_{\mathbb{k}}(f, x). $$$

Lean4

theorem differentiableAt (f : V →ᴬ[𝕜] W) {x : V} : DifferentiableAt 𝕜 f x :=
  f.differentiable x

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

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

Разделы

Аффилиация

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