OAI/Geometry/HyperbolicGroups/IndexedPayment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.FanLink.IndexedFanData.PaymentIndex line 18

   Source documentation

   Outgoing and incoming exceptional-port incidences of selected top turns.

   abbrev PaymentIndex := {p : (Σ z,L z) × Bool //
   …

2. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.paymentIndex_card line 22
3. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.family_natPaymentIndex_card line 42