OAI/Geometry/HyperbolicGroups/RelativeInteriorCount.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.exterior_length line 26
2. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.interior_mem line 30
3. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.exterior_face_unique line 34
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.interior_card line 51

   Source documentation

   Exactly one face is exterior, even with free outside-to-outside folds.

   lemma interior_card : (Fintype.card (InteriorFace n w d ell hell word c hc f P) : ℤ) =
       cycles P.pairing.face - 1 := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.InteriorFace

5. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.outside_contacts_le line 74