OAI/Geometry/HyperbolicGroups/PictureDual.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.dual line 19

   Source documentation

   Literal rotation-system duality: faces and vertices exchange, while individual edge-side copies and their pairing are unchanged.

   def dual : PictureMap D where
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap

2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.dual_edge line 25
3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.dual_face line 26
4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.dual_vertex line 27
5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.dual_dual line 30
6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.dual_components line 39
7. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.dual_euler line 56
8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.dual_genusZero line 60