contDiffOn_const

Mathlib.Analysis.Calculus.ContDiff.Basic

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

English

A constant map restricted to a set is ContDiffWithinAt at a point.

Русский

Ограничение константной карты на множество обладает ContDiffWithinAt в точке.

LaTeX

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

Lean4

@[fun_prop]
theorem contDiffOn_const {c : F} {s : Set E} : ContDiffOn 𝕜 n (fun _ : E => c) s :=
  contDiff_const.contDiffOn

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

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

Разделы

Аффилиация

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