u_neg

Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

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

English

For all x, u(x) ≥ 0.

Русский

Для всех x выполняется u(x) ≥ 0.

LaTeX

$$$\\forall x, 0 \\le u(x)$$$

Lean4

theorem u_neg (x : E) : u (-x) = u x :=
  (Classical.choose_spec (u_exists E)).2.2.2 x

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

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

Разделы

Аффилиация

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