norm_def' — Mathlib

English

Let M be a C*-matrix with entries in a nonunital C*-algebra A. The norm of M equals the norm of its associated nonunital algebra hom image, i.e., ‖M‖ = ‖Φ(M)‖ for the canonical Φ from CStarMatrix to the corresponding operator realization.

Русский

Пусть M — матрица над ненулевой C*-алгеброй A. Норма M совпадает с нормой образа под каноническим отображением в непрерывный линейный оператор: ‖M‖ = ‖Φ(M)‖, где Φ — соответствующее отображение.

LaTeX

$$$$\\|M\\| = \\|\\Phi(M)\\|,$$$$

Lean4

theorem norm_def' {M : CStarMatrix n n A} : ‖M‖ = ‖toCLMNonUnitalAlgHom (A := A) M‖ :=
  rfl

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