norm_eq — Mathlib

English

In a finite product of normed spaces, the norm is the square root of the sum of the squares of the coordinate norms: ∥x∥ = sqrt( ∑_i ∥x_i∥^2 ).

Русский

В конечном произведении нормированных пространств норма равна корню из суммы квадратов норм координат: ∥x∥ = sqrt( ∑_i ∥x_i∥^2 ).

LaTeX

$$$\|x\| = \sqrt{ \sum_i \|x_i\|^2 }$$$

Lean4

theorem norm_eq {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n] (x : EuclideanSpace 𝕜 n) : ‖x‖ = √(∑ i, ‖x i‖ ^ 2) := by
  simpa only [Real.coe_sqrt, NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) x.nnnorm_eq

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