OAI/Geometry/HyperbolicGroups/RelativeSlots.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.SelectedTopFace line 24
2. instance OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.(instance at line 25) line 25
3. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.faceOccurrence line 27
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.faceOccurrence_kind line 28
5. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.topSlot line 31
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.topSlot_injective line 37
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.topSlot_surjective line 45
8. theorem OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.fragment_slots_eq line 60

   Source documentation

   Each selected top polygon contributes all seven indexed fan slots, including the fan slots its simple boundary omits.

   theorem fragment_slots_eq :
       (∑ b : Fan n w, Fintype.card (SelectedTop n w d ell hell word c hc f P select b)) =
         7 * Fintype.card (SelectedTopFace n w d ell hell word c hc f P select) := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Fan, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.SelectedTop, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.SelectedTopFace