hasCompactSupport_normed

Mathlib.Analysis.Calculus.BumpFunction.Normed

URI: https://scilib.ai/kg/mathlib#ContDiffBump.hasCompactSupport_normed

← MathLib Explorer

English

The normed bump f.normed μ has compact support.

Русский

Нормированная бу́мпа f.normed μ имеет компактную опору.

LaTeX

$$$ \mathrm{HasCompactSupport}(f.normed\mu) $$$

Lean4

theorem hasCompactSupport_normed : HasCompactSupport (f.normed μ) := by
  simp only [HasCompactSupport, f.tsupport_normed_eq (μ := μ), isCompact_closedBall]

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

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

Разделы

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

Аффилиация

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