OAI/Geometry/HyperbolicGroups/PermErase.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicObstruction.PictureSwitch.sameCycle_setoid_merge_left line 16
  2. def OAI.HyperbolicObstruction.PictureSwitch.bypass line 35

    Source documentation

    Fix the punctured point and bypass it in its original cycle. Restricting this permutation to the complement literally erases that indexed corner.

    def bypass (p : Perm D) (a : D) : Perm D := swap a (p a) * p
  3. lemma OAI.HyperbolicObstruction.PictureSwitch.bypass_fixed line 37
  4. lemma OAI.HyperbolicObstruction.PictureSwitch.bypass_away line 40
  5. lemma OAI.HyperbolicObstruction.PictureSwitch.bypass_invariant line 46
  6. def OAI.HyperbolicObstruction.PictureSwitch.erase line 51
  7. lemma OAI.HyperbolicObstruction.PictureSwitch.bypass_orbits line 56
  8. lemma OAI.HyperbolicObstruction.PictureSwitch.erase_orbits line 75
  9. lemma OAI.HyperbolicObstruction.PictureSwitch.bypass_cycles line 80
  10. lemma OAI.HyperbolicObstruction.PictureSwitch.erase_cycles line 87