OAI/Geometry/HyperbolicGroups/RelativePayment.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.top_exceptional_incoming line 25
2. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.AllPaymentIndex line 51
3. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.paymentCorner line 54
4. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.paymentBool line 55
5. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.paymentRawDart line 57
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.payment_raw_index line 63
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.payment_selected line 86
8. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.payment_param_injective line 94
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.paymentRawDart_injective line 110
10. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.allPaymentIndex_card line 132