instNormForall — Mathlib

English

Define a norm on the product space C⋆ᵐᵒᵈ(A, Π_i E_i) by norm(x) = sqrt( || ∑_i ⟪x_i, x_i⟫_A || ).

Русский

Задаётся норма на произведении: для x = (x_i)_i в пространстве Π_i E_i пусть ∥x∥ = sqrt( || ∑_i ⟪x_i, x_i⟫_A || ).

LaTeX

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

Lean4

noncomputable instance : Norm C⋆ᵐᵒᵈ(A, Π i, E i) where norm x := √‖∑ i, ⟪x i, x i⟫_A‖

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