hasNorm — Mathlib

English

The norm on the space of continuous affine maps is defined as the maximum of the value at 0 and the operator norm of the linear part.

Русский

Норма пространства непрерывных аффинных отображений определяется как максимум между значением в 0 и нормой линейной части.

LaTeX

$$$$\|f\| = \max\{ \|f(0)\|, \|f.contLinear\|\}.$$$$

Lean4

/-- Note that unlike the operator norm for linear maps, this norm is _not_ submultiplicative:
we do _not_ necessarily have `‖f.comp g‖ ≤ ‖f‖ * ‖g‖`. See `norm_comp_le` for what we can say. -/
noncomputable instance hasNorm : Norm (V →ᴬ[𝕜] W) :=
  ⟨fun f => max ‖f 0‖ ‖f.contLinear‖⟩

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