norm_eq_sqrt_re_inner — Mathlib

English

For F with Real inner product, ‖x‖ = √⟪x, x⟫_ℝ.

Русский

Для вещественного пространства с внутренним произведением ‖x‖ = √⟪x, x⟫_ℝ.

LaTeX

$$$\|x\| = \sqrt{\langle x, x\rangle_ℝ}$$$

Lean4

theorem norm_eq_sqrt_re_inner (x : E) : ‖x‖ = √(re ⟪x, x⟫) :=
  calc
    ‖x‖ = √(‖x‖ ^ 2) := (sqrt_sq (norm_nonneg _)).symm
    _ = √(re ⟪x, x⟫) := congr_arg _ (norm_sq_eq_re_inner _)

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