norm_def

Mathlib.Analysis.Normed.Group.Hom

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

English

The norm of a morphism is the same as the operator norm defined via the infimum of bounds.

Русский

Норма морфизма равна операторной норме, определяемой через инфimum ограничений.

LaTeX

$$$‖f‖ = \\operatorname{hasOpNorm.norm}(f)$$$

Lean4

theorem norm_def : ‖f‖ = sInf {c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖} :=
  rfl

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

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

Разделы

Аффилиация

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