w_mul_φ_nonneg

Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

URI: https://scilib.ai/kg/mathlib#ExistsContDiffBumpBase.w_mul_φ_nonneg

← MathLib Explorer

English

The product w(D,y) · φ(x−y) is nonnegative for all x,y and D.

Русский

Произведение w(D,y) φ(х−у) неотрицательно для всех x,y и D.

LaTeX

$$$0 \\le w(D,y) \\cdot \\phi(x-y)$$$

Lean4

theorem w_mul_φ_nonneg (D : ℝ) (x y : E) : 0 ≤ w D y * φ (x - y) :=
  mul_nonneg (w_nonneg D y) (indicator_nonneg (by simp only [zero_le_one, imp_true_iff]) _)

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

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

Разделы

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

Аффилиация

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