nonneg'

Mathlib.Analysis.Calculus.BumpFunction.Basic

URI: https://scilib.ai/kg/mathlib#ContDiffBump.nonneg'

English

For any x, f x ≥ 0.

Русский

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

LaTeX

$$$ 0 \le f(x). $$$

Lean4

/-- A version of `ContDiffBump.nonneg` with `x` explicit -/
theorem nonneg' (x : E) : 0 ≤ f x :=
  f.nonneg

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

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

Разделы

Аффилиация

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