prod_norm — Mathlib

English

The norm on the product space equals the Euclidean norm of the pair of norms: ∥(x,y)∥ = sqrt(∥x∥^2 + ∥y∥^2).

Русский

Норма на произведении пространства равна евклидовой норме пары норм: ∥(x,y)∥ = sqrt(∥x∥^2 + ∥y∥^2).

LaTeX

$$$\\| (x,y) \\| = \\sqrt{\\|x\\|^{2} + \\|y\\|^{2}}$$$

Lean4

theorem prod_norm (x : C⋆ᵐᵒᵈ(A, E × F)) : ‖x‖ = √‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖ :=
  rfl

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