OAI/Geometry/HyperbolicGroups/PictureMirror.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.cycles_inverse line 16
2. lemma OAI.HyperbolicObstruction.PictureSwitch.cycles_conjugate line 19
3. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.reverse line 26
4. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mirror line 42

   Source documentation

   Reflection reverses every face orientation; side pairs are unchanged.

   def mirror : PictureMap D where
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap

5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mirror_components line 49
6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mirror_euler line 62
7. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mirror_genusZero line 73