Theorems · Definition · functional analysis

CStarAlgebra.spectralOrder

(A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A

The partial order on a C⋆-algebra defined by x ≤ y if and only if y - x is selfadjoint and has nonnegative spectrum. This is not declared as an instance because one may already have a partial order with better definitional properties. However, it can be useful to invoke this as an instance in proofs.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Cited by

2 results in Mathlib

Foundations

Depth 314 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonUnitalCStarAlgebra