OAI/Analysis/Pureness/Completion/CompletedRankExhaustion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.CuntzSubequiv.inr line 11
2. theorem OAI.CuntzPureness.CuntzSubequiv.completedRank_le line 20
3. theorem OAI.CuntzPureness.completedRootRank_cut_le line 25
4. theorem OAI.CuntzPureness.completedRootRank_eq_iSup_cuts line 30
5. theorem OAI.CuntzPureness.completedRootRank_cuts_tendsto line 35
6. theorem OAI.CuntzPureness.completedRootRank_mono_positive line 41
7. theorem OAI.CuntzPureness.completedRootRank_polar line 47