toNorm — Mathlib

English

The norm on the space is defined by the real part of the scalar product with itself: ‖x‖ = √(Re ⟪x, x⟫). This defines a (semi)norm coming from the core.

Русский

Норма на пространстве задаётся как ‖x‖ = √(Re ⟪x, x⟫); это (псевдонормированная) норма, порожденная ядром.

LaTeX

$$$\|x\| = \sqrt{\operatorname{Re}\langle x,x\rangle}$$$

Lean4

/-- (Semi)norm constructed from a `PreInnerProductSpace.Core` structure, defined to be the square
root of the scalar product. -/
def toNorm : Norm F where norm x := √(re ⟪x, x⟫)

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