w_nonneg

Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

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

← MathLib Explorer

English

The auxiliary function w is always nonnegative for all D and x.

Русский

Вспомогательная функция w во всех случаях D и x неотрицательна.

LaTeX

$$$0 \\le w(D,x)$$$

Lean4

theorem w_nonneg (D : ℝ) (x : E) : 0 ≤ w D x :=
  by
  apply mul_nonneg _ (u_nonneg _)
  apply inv_nonneg.2
  apply mul_nonneg (u_int_pos E).le
  norm_cast
  apply pow_nonneg (abs_nonneg D)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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