contDiffAt

Mathlib.Analysis.Calculus.BumpFunction.Basic

URI: https://scilib.ai/kg/mathlib#ContDiffBump.contDiffAt

English

The bump function is ContDiffAt of order n at every point x, i.e. its pointwise differentiability matches the global differentiability assumptions.

Русский

Бамп-функция является ContDiffAt порядка n в каждой точке x.

LaTeX

$$$\\forall {c:g}, {f: ContDiffBump c}, {x}, ContDiffAt Real (WithTop.some n) f.toFun x$$$

Lean4

protected theorem contDiffAt : ContDiffAt ℝ n f x :=
  f.contDiff.contDiffAt

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

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

Разделы

Аффилиация

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