OAI/Geometry/HyperbolicGroups/ContactCapacity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.PictureSwitch.PictureMap.IncidentContact line 17
2. abbrev OAI.HyperbolicObstruction.PictureSwitch.PictureMap.PositionSide line 18
3. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.contactEnd line 20
4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.contactEnd_position line 24
5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.contactEnd_injective line 31
6. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.contact_capacity line 40

   Source documentation

   Contacts charge actual side copies injectively, even if the contact graph has cycles or parallel edges. This is not a forest assumption.

   theorem contact_capacity : Fintype.card (P.IncidentContact selected raw position p) ≤
       Fintype.card (PositionSide selected raw position p) := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.PositionSide