OAI/Analysis/Pureness/Cuntz/SharedCuntzBridge.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CuntzPureness.cuntzSubequiv_iff_shared line 12
2. def OAI.CuntzPureness.completedSharedClass line 18
3. lemma OAI.CuntzPureness.shared_positive_roundtrip line 22
4. lemma OAI.CuntzPureness.shared_cuntz_map_equiv line 28
5. theorem OAI.CuntzPureness.completedSharedClass_le_iff line 43
6. theorem OAI.CuntzPureness.completedSharedClass_surjective line 48
7. theorem OAI.CuntzPureness.shared_zero_sandwich line 57