w_compact_support

Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

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

← MathLib Explorer

English

Another formulational variant expressing the integral of w with the same normalization.

Русский

Еще одно выражение нормы интеграла для той же функции w.

LaTeX

$$$\\int_E w(D,x)\\,d\\mu(x)=1$$$

Lean4

theorem w_compact_support {D : ℝ} (Dpos : 0 < D) : HasCompactSupport (w D : E → ℝ) :=
  by
  rw [hasCompactSupport_def, w_support E Dpos, closure_ball (0 : E) Dpos.ne']
  exact isCompact_closedBall _ _

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

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

Разделы

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

Аффилиация

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