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

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.

@[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.