u_continuous

Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

URI: https://scilib.ai/kg/mathlib#ExistsContDiffBumpBase.u_continuous

English

u is a continuous bump base function; its symmetry and support hold.

Русский

u — непрерывная база бамп-функций; соблюдаются симметричность и опоры.

LaTeX

$$$u\\text{ is a continuous bump base with support ball 0 1 and symmetry.}$$$

Lean4

theorem u_continuous : Continuous (u : E → ℝ) :=
  (u_smooth E).continuous

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

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

Разделы

Аффилиация

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