contDiffWithinAt_const

Mathlib.Analysis.Calculus.ContDiff.Basic

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

English

A constant function restricted to a set is ContDiffWithinAt at every point.

Русский

Ограничение константной функции на множество гладно в каждой точке.

LaTeX

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

Lean4

@[fun_prop]
theorem contDiffWithinAt_const {c : F} : ContDiffWithinAt 𝕜 n (fun _ : E => c) s x :=
  contDiffAt_const.contDiffWithinAt

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

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

Разделы

Аффилиация

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