OAI/Analysis/Pureness/Stabilization/RankFunctorial.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzTrace.Positive.map_power line 13
2. theorem OAI.CuntzTrace.ExtendedTrace.rank_zero_trace line 27
3. theorem OAI.CuntzTrace.ExtendedTrace.rank_add line 30
4. theorem OAI.CuntzTrace.ExtendedTrace.rank_pullback line 35
5. theorem OAI.CuntzTrace.ExtendedTrace.rank_le_liminf_of_canonicalConverges line 42