OAI/Geometry/HyperbolicGroups/ActualRawCount.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.DecorationSideIndex line 25
2. def OAI.HyperbolicObstruction.ConeSkeleton.decorationRawDart line 28
3. lemma OAI.HyperbolicObstruction.ConeSkeleton.decorationRawDart_injective line 31
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.decorationRawDart_raw line 44
5. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RawAccountIndex line 55
6. def OAI.HyperbolicObstruction.ConeSkeleton.accountDart line 59
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.accountDart_injective line 64
8. lemma OAI.HyperbolicObstruction.ConeSkeleton.accountDart_selected line 102
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.accountDart_raw line 111
10. lemma OAI.HyperbolicObstruction.ConeSkeleton.actual_raw_account_le line 125