nonneg

Mathlib.Geometry.Manifold.BumpFunction

URI: https://scilib.ai/kg/mathlib#SmoothBumpFunction.nonneg

English

For all x, f(x) ≥ 0.

Русский

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

LaTeX

$$$\forall x, \; 0 \le f(x).$$$

Lean4

theorem nonneg : 0 ≤ f x :=
  f.mem_Icc.1

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

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

Разделы

Аффилиация

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