contDiff_normed

Mathlib.Analysis.Calculus.BumpFunction.Normed

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

English

The normed bump is continuously differentiable to the requested order n, i.e., ContDiff with respect to the real parameter.

Русский

Нормированное bump гладко дифференцируемо до нужного порядка n: ContDiff по параметру.

LaTeX

$$ContDiff Real (WithTop.some n) (f.normed μ)$$

Lean4

theorem contDiff_normed {n : ℕ∞} : ContDiff ℝ n (f.normed μ) :=
  f.contDiff.div_const _

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

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

Разделы

Аффилиация

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