OAI/Geometry/HyperbolicGroups/PermErasePair.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.PictureSwitch.OffPair line 16
2. lemma OAI.HyperbolicObstruction.PictureSwitch.offPair_invariant line 18
3. lemma OAI.HyperbolicObstruction.PictureSwitch.bypass_keeps_fixed line 27
4. def OAI.HyperbolicObstruction.PictureSwitch.bypassPair line 31
5. lemma OAI.HyperbolicObstruction.PictureSwitch.bypassPair_a line 33
6. lemma OAI.HyperbolicObstruction.PictureSwitch.bypassPair_b line 35
7. def OAI.HyperbolicObstruction.PictureSwitch.erasePair line 37
8. lemma OAI.HyperbolicObstruction.PictureSwitch.erasePair_orbits line 42
9. lemma OAI.HyperbolicObstruction.PictureSwitch.card_offPair line 50
10. lemma OAI.HyperbolicObstruction.PictureSwitch.erasePair_cycles line 58