OAI/Geometry/HyperbolicGroups/PictureSum.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.cycles_sum line 19
2. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.sum line 61

   Source documentation

   Literal disjoint union of polygon side-pairings.

   def sum : PictureMap (D ⊕ E) where
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap

3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.sum_vertex line 73
4. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.sumClassifier line 77
5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.sum_components line 81
6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.sum_components_card line 113
7. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.sum_not_components line 121
8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.sum_euler line 125
9. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.sum_genusZero line 133