norm_map — Mathlib

English

For a star-equivalence φ between nonunital C*-algebras, the nn-norm is preserved by φ and its inverse, i.e., ‖φ(a)‖₊ = ‖a‖₊.

Русский

Пусть φ — звёздный эквивалент между неполными C*-алгебрами; тогда nnnorm сохраняется под φ и его обратным, то есть ‖φ(a)‖₊ = ‖a‖₊.

LaTeX

$$$\|\phi(a)\|_{nn} = \|a\|_{nn}$$$

Lean4

theorem norm_map (φ : F) (a : A) : ‖φ a‖ = ‖a‖ :=
  congr_arg NNReal.toReal (nnnorm_map φ a)

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