norm_def

Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

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

English

The operator norm of the linear part is bounded above by the norm of the affine map.

Русский

Нормa линейной части ограничена нормой аффинного отображения.

LaTeX

$$$$\|f.contLinear\| \leq \|f\|.$$$$

Lean4

theorem norm_def : ‖f‖ = max ‖f 0‖ ‖f.contLinear‖ :=
  rfl

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

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

Разделы

Аффилиация

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