instNorm

Mathlib.Topology.ContinuousMap.Bounded.Normed

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.instNorm

English

The space of bounded continuous functions is equipped with a norm, defined as the distance to the zero function.

Русский

Эти функции образуют нормированное пространство: норма равна расстоянию до нуля.

LaTeX

$$$Norm (\\alpha \\to^{\\mathrm{b}} \\beta)$$$

Lean4

instance instNorm : Norm (α →ᵇ β) :=
  ⟨(dist · 0)⟩

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

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

Разделы

Аффилиация

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