OAI/Analysis/JiangSu/CStarAlgebras/CompletedRankExhaustion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Pureness.CuntzSubequiv.inr line 18
2. theorem OAI.Pureness.CuntzSubequiv.completedRank_le line 27
3. theorem OAI.Pureness.completedRootRank_cut_le line 32
4. theorem OAI.Pureness.completedRootRank_eq_iSup_cuts line 37
5. theorem OAI.Pureness.completedRootRank_cuts_tendsto line 42
6. theorem OAI.Pureness.completedRootRank_mono_positive line 48
7. theorem OAI.Pureness.completedRootRank_polar line 54