mdifferentiableAt_const

Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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

English

A constant map is differentiable at every point.

Русский

Константное отображение дифференцируемо во всех точках.

LaTeX

$$$ mdifferentiableAt I I' (\lambda _ : M => c) x $$$

Lean4

theorem mdifferentiableAt_const : MDifferentiableAt I I' (fun _ : M => c) x :=
  (hasMFDerivAt_const c x).mdifferentiableAt

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

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

Разделы

Аффилиация

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