u_nonneg

Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

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

English

The bump base u is even: u(-x)=u(x).

Русский

База bump‑функций нечетная: u(-x)=u(x).

LaTeX

$$$u(-x) = u(x)$$$

Lean4

theorem u_nonneg (x : E) : 0 ≤ u x :=
  ((Classical.choose_spec (u_exists E)).2.1 x).1

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

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

Разделы

Аффилиация

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