OAI/Geometry/HyperbolicGroups/BigonRemove.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HyperbolicObstruction.PictureSwitch.PictureMap.Bigon line 21
2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.Bigon.face_invariant line 30
3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.Bigon.switching_vertex line 35
4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.Bigon.switched_pair line 41
5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.Bigon.switched_back line 45
6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.Bigon.edge_invariant line 49
7. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.Bigon.remove line 59

   Source documentation

   The zero-chain backtracking bigon is first pinched off by a legal vertex switch and then deleted as a whole component. Its other edge contacts need not initially meet one another.

   def remove : PictureMap {x // OffPair a b x} :=
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap, OAI.HyperbolicObstruction.PictureSwitch.OffPair

8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.Bigon.remove_face line 62
9. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.Bigon.remove_genusZero line 64
10. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.Bigon.remove_respects line 69
11. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.Bigon.remove_closed line 75
12. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.Bigon.remove_kind line 79