contMDiffAt

Mathlib.Geometry.Manifold.BumpFunction

URI: https://scilib.ai/kg/mathlib#SmoothBumpFunction.contMDiffAt

English

For every x, the bump f is infinitely differentiable at x in the manifold sense.

Русский

Для каждого x шляпочная функция гладкая в точке x в смысле ContMDiffAt.

LaTeX

$$ContMDiffAt I 𝓘(ℝ) ∞ f x$$

Lean4

protected theorem contMDiffAt {x} : ContMDiffAt I 𝓘(ℝ) ∞ f x :=
  f.contMDiff.contMDiffAt

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

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

Разделы

Аффилиация

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