u_support

Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

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

English

HasCompactSupport of u holds; its support is contained in the unit ball.

Русский

У функции u компактная опора, включенная в единичный шар.

LaTeX

$$$\\operatorname{HasCompactSupport}(u)$ and ${\\rm supp}(u) = \\mathrm{ball}(0,1)$$$

Lean4

theorem u_support : support (u : E → ℝ) = ball 0 1 :=
  (Classical.choose_spec (u_exists E)).2.2.1

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

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

Разделы

Аффилиация

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