u_le_one

Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

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

English

For all x, u(x) ≤ 1.

Русский

Для всех x верно u(x) ≤ 1.

LaTeX

$$$\\forall x,\\; u(x) \\le 1$$$

Lean4

theorem u_le_one (x : E) : u x ≤ 1 :=
  ((Classical.choose_spec (u_exists E)).2.1 x).2

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

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

Разделы

Аффилиация

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