norm_def

Mathlib.Topology.ContinuousMap.Bounded.Normed

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

English

The norm of a bounded continuous function equals the distance to the zero function: ‖f‖ = dist f 0.

Русский

Норма ограниченно непрерывной функции равна расстоянию до нулевой функции: ‖f‖ = dist f 0.

LaTeX

$$$‖f‖ = \\mathrm{dist}(f,0)$$$

Lean4

theorem norm_def : ‖f‖ = dist f 0 :=
  rfl

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

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

Разделы

Аффилиация

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