toNormedSpace — Mathlib

English

The core induces a normed space structure on F, with norm defined by √(Re ⟪x,x⟫).

Русский

Ядро порождает нормированное пространство на F, с нормой √(Re ⟪x,x⟫).

LaTeX

$$$\|x\| = \sqrt{\operatorname{Re}\langle x,x\rangle}$ and the induced structure is a NormedSpace$$

Lean4

/-- Normed space (which is actually a seminorm in general) structure constructed from a
`PreInnerProductSpace.Core` structure -/
def toNormedSpace : NormedSpace 𝕜 F where
  norm_smul_le r
    x := by
    rw [norm_eq_sqrt_re_inner, inner_smul_left, inner_smul_right, ← mul_assoc]
    rw [RCLike.conj_mul, ← ofReal_pow, re_ofReal_mul, sqrt_mul, ← ofReal_normSq_eq_inner_self, ofReal_re]
    · simp [sqrt_normSq_eq_norm]
    · positivity

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