OAI/Geometry/HyperbolicGroups/RelativeRawCount.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.DecorationSideIndex line 29
2. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.decorationRawDart line 32
3. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.decorationRawDart_injective line 35
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.decorationRawDart_raw line 48
5. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.RawAccountIndex line 59
6. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.accountDart line 63
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.accountDart_injective line 68
8. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.accountDart_selected line 106
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.accountDart_raw line 115
10. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_raw_account_le line 129