continuous_normed

Mathlib.Analysis.Calculus.BumpFunction.Normed

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

English

The normed bump is a continuous function from E to R when viewed as a function of the point x.

Русский

Нормированное bump — непрерывная функция от E в R как функция от точки x.

LaTeX

$$Continuous (f.normed μ)$$

Lean4

theorem continuous_normed : Continuous (f.normed μ) :=
  f.continuous.div_const _

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

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

Разделы

Аффилиация

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