contDiffAt_const

Mathlib.Analysis.Calculus.ContDiff.Basic

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

English

A constant map is ContDiffAt at any point.

Русский

Константное отображение гладко в любой точке (ContDiffAt).

LaTeX

$$$\\text{ContDiffAt } 𝕜 n (\\lambda x. c) x$$$

Lean4

@[fun_prop]
theorem contDiffAt_const {c : F} : ContDiffAt 𝕜 n (fun _ : E => c) x :=
  contDiff_const.contDiffAt

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

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

Разделы

Аффилиация

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