normedSpace — Mathlib

English

L carries a norm and a compatible scalar action by K, turning it into a normed space over K with norm defined by spectralNorm.

Русский

L обладает нормой и совместным действием скаляров из K, превращая его в нормированное пространство над K, нормой является spectralNorm.

LaTeX

$$$\|\cdot\|: L \to \mathbb{R}_{\ge 0}$, \|r \cdot x\| \le \|r\| \|x\|$$$

Lean4

/-- `L` with the spectral norm is a `normed_space` over `K`. -/
def normedSpace [CompleteSpace K] : @NormedSpace K L _ (seminormedAddCommGroup K L) :=
  letI _ := seminormedAddCommGroup K L
  { (inferInstance : Module K L) with
    norm_smul_le r
      x := by
      change spectralAlgNorm K L (r • x) ≤ ‖r‖ * spectralAlgNorm K L x
      exact le_of_eq (map_smul_eq_mul _ _ _) }

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