isometry — Mathlib

English

Any star-algebra equivalence between nonunital complex C*-algebras is an isometry with respect to the canonical norm.

Русский

Любые звездно-алгебраические эквиваленты между неполными комплексными C*-алгебрами являются изометриями по стандартной норме.

LaTeX

$$$\text{Isometry}(\varphi)$ for a star-equivalence $\varphi$$$

Lean4

theorem isometry (φ : F) : Isometry φ :=
  AddMonoidHomClass.isometry_of_norm φ (norm_map φ)

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