Documentation

Mathlib.Analysis.CStarAlgebra.Extreme

Extreme points of the closed unit ball in C⋆-algebras #

This file contains results on the extreme points of the closed unit ball in (unital) C⋆-algebras.

References #

C⋆-algebras and W⋆-algebras

source
theorem isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {e : A} :
IsStarProjection e ↔ e ∈ Set.extremePoints ℝ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 1)

The star projections in a non-unital C⋆-algebra are exactly the extreme points of the nonnegative closed unit ball.

source
@[deprecated isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall (since := "2026-07-09")]
theorem isStarProjection_iff_mem_extremePoints_setOf_nonneg_inter_unitClosedBall {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {e : A} :
IsStarProjection e ↔ e ∈ Set.extremePoints ℝ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 1)

Alias of isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall.

The star projections in a non-unital C⋆-algebra are exactly the extreme points of the nonnegative closed unit ball.