Theorem CStarAlgebra.directedOn_nonneg_ball

Modification history

2024-10-30 16:54
Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
feat: positive contractions in a Cā‹†-algebra form a directed set (#18016)
Added CStarAlgebra.directedOn_nonneg_ballView on Github ā†’