OAI/GroupTheory/Hyperbolic/Links.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Release075.MarkedLineData.ODirections line 8
  2. abbrev OAI.Release075.MarkedLineData.VDirections line 9
  3. abbrev OAI.Release075.MarkedLineData.WDirections line 10
  4. abbrev OAI.Release075.MarkedLineData.AllDirections line 11
  5. def OAI.Release075.MarkedLineData.allLink line 15

    Source documentation

    At O a larger complete bipartite graph suffices for the four-edge girth bound; at V and W we use precisely the shifted incidence links.

    noncomputable def allLink : SimpleGraph (d.AllDirections hr) :=
…
  6. def OAI.Release075.MarkedLineData.linkDirection line 19
  7. def OAI.Release075.MarkedLineData.linkColor line 27
  8. theorem OAI.Release075.MarkedLineData.linkDirection_color line 32
  9. theorem OAI.Release075.MarkedLineData.linkDirection_injective line 38
  10. theorem OAI.Release075.MarkedLineData.face_corner_adj line 45
  11. theorem OAI.Release075.MarkedLineData.allLink_closed line 55
  12. theorem OAI.Release075.MarkedLineData.v_reduced_same_label line 81
  13. theorem OAI.Release075.MarkedLineData.w_reduced_same_label line 94
  14. theorem OAI.Release075.MarkedLineData.x_turn_large line 114
  15. abbrev OAI.Release075.MarkedLineData.concreteRibbon line 143
  16. def OAI.Release075.MarkedLineData.dartDirection line 146
  17. theorem OAI.Release075.MarkedLineData.ribbon_outer_iff line 149
  18. theorem OAI.Release075.MarkedLineData.ribbon_color line 153
  19. theorem OAI.Release075.MarkedLineData.ribbon_direction_step line 160
  20. theorem OAI.Release075.MarkedLineData.ribbon_adj line 166
  21. theorem OAI.Release075.MarkedLineData.ribbon_reduced line 174
  22. theorem OAI.Release075.MarkedLineData.ribbon_closed line 190