instPartialOrder — Mathlib

English

The unitization A⁺¹ of a nonunital C*-algebra A is equipped with a natural partial order, namely the spectral order, making A⁺¹ into a partially ordered algebra extending the order on A via its embedding into A⁺¹.

Русский

Единичизация A⁺¹ неюнитированной C*-алгебры A оснащена естественным частичным порядком, называемым спектральным порядком, который превращает A⁺¹ в частично упорядкованную алгебру, расширяющую существующий порядок на A через встраивание A в A⁺¹.

LaTeX

$$$A^{+1}$ carries the spectral order $\le_{sp}$ on its underlying set, extending the order on $A$.$$

Lean4

noncomputable instance instPartialOrder : PartialOrder A⁺¹ :=
  CStarAlgebra.spectralOrder _

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