nontriviallyNormedField — Mathlib

English

The spectral norm makes L a nontrivially normed field; there exists a nonzero element with positive norm.

Русский

Спектральная норма превращает L в ненулево нормированное поле: существует ненулевой элемент с положительной нормой.

LaTeX

$$$\exists x\,(x \neq 0) \land \mathrm{spectralNorm}(K,L,x) > 0$$$

Lean4

/-- `L` with the spectral norm is a `NontriviallyNormedField`. -/
def nontriviallyNormedField [CompleteSpace K] : NontriviallyNormedField L
    where
  __ := spectralNorm.normedField K L
  non_trivial :=
    let ⟨x, hx⟩ := NontriviallyNormedField.non_trivial (α := K)
    ⟨algebraMap K L x, hx.trans_eq <| (spectralNorm_extends _).symm⟩

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