pi_norm — Mathlib

English

For the family E_i, the norm on the product is given by ‖x‖ = √‖∑_i ⟪x_i, x_i⟫_A‖.

Русский

Для семейства пространств E_i норма на произведение равна ‖x‖ = √‖∑_i ⟪x_i, x_i⟫_A‖.

LaTeX

$$$\\|x\\| = \\sqrt{\\|\\sum_i \\langle x_i, x_i \\rangle_A\\|}$$$

Lean4

theorem pi_norm (x : C⋆ᵐᵒᵈ(A, Π i, E i)) : ‖x‖ = √‖∑ i, ⟪x i, x i⟫_A‖ := by with_reducible_and_instances rfl

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