OAI/Geometry/HyperbolicGroups/WalkPayment.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.top_exceptional_incoming line 26
2. abbrev OAI.HyperbolicObstruction.ConeSkeleton.AllPaymentIndex line 52
3. abbrev OAI.HyperbolicObstruction.ConeSkeleton.paymentCorner line 55
4. abbrev OAI.HyperbolicObstruction.ConeSkeleton.paymentBool line 56
5. def OAI.HyperbolicObstruction.ConeSkeleton.paymentRawDart line 58
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.payment_raw_index line 64
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.payment_selected line 87
8. lemma OAI.HyperbolicObstruction.ConeSkeleton.payment_param_injective line 95
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.paymentRawDart_injective line 111
10. lemma OAI.HyperbolicObstruction.ConeSkeleton.allPaymentIndex_card line 133