tsupport_normed_eq

Mathlib.Analysis.Calculus.BumpFunction.Normed

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

← MathLib Explorer

English

The topological support of the normed bump is exactly the closed ball around c with radius rOut.

Русский

Пусть tsupport нормы бу́мпы — это замкнутый шар вокруг c радиуса rOut.

LaTeX

$$$ \mathrm{tsupport}(f.normed \mu) = \mathrm{closedBall}(c, f.rOut) $$$

Lean4

theorem tsupport_normed_eq : tsupport (f.normed μ) = Metric.closedBall c f.rOut := by
  rw [tsupport, f.support_normed_eq, closure_ball _ f.rOut_pos.ne']

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

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

Разделы

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

Аффилиация

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