OAI/Topology/EilenbergGanea/SeedConnection.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EilenbergGanea.SeedConnection.circleWord line 14
  2. def OAI.EilenbergGanea.SeedConnection.boundaryEdgeWord line 16
  3. def OAI.EilenbergGanea.SeedConnection.boundaryWords line 20
  4. theorem OAI.EilenbergGanea.SeedConnection.boundaryWords_prod line 23
  5. theorem OAI.EilenbergGanea.SeedConnection.sector_end line 26
  6. theorem OAI.EilenbergGanea.SeedConnection.circle_distinct line 30
  7. theorem OAI.EilenbergGanea.SeedConnection.sector_distinct line 32
  8. def OAI.EilenbergGanea.SeedConnection.circleLabel line 34
  9. def OAI.EilenbergGanea.SeedConnection.radialLabel line 36
  10. theorem OAI.EilenbergGanea.SeedConnection.boundaryWords_length line 39
  11. theorem OAI.EilenbergGanea.SeedConnection.boundaryWords_get line 42
  12. theorem OAI.EilenbergGanea.SeedConnection.radial_step line 46
  13. def OAI.EilenbergGanea.SeedConnection.edgeAnchor line 70
  14. def OAI.EilenbergGanea.SeedConnection.edgeLocal line 74
  15. def OAI.EilenbergGanea.SeedConnection.faceLocal line 78
  16. theorem OAI.EilenbergGanea.SeedConnection.edgeLocal_anchor line 82
  17. theorem OAI.EilenbergGanea.SeedConnection.nextSector_first line 85
  18. theorem OAI.EilenbergGanea.SeedConnection.faceLocal_incidence line 87
  19. def OAI.EilenbergGanea.SeedConnection.cellRank line 115
  20. theorem OAI.EilenbergGanea.SeedConnection.properFace_rank line 120
  21. theorem OAI.EilenbergGanea.SeedConnection.properFace_trans line 124
  22. def OAI.EilenbergGanea.SeedConnection.upLabel line 130
  23. theorem OAI.EilenbergGanea.SeedConnection.upLabel_diag line 136
  24. theorem OAI.EilenbergGanea.SeedConnection.upLabel_same_rank line 139
  25. theorem OAI.EilenbergGanea.SeedConnection.upLabel_trans line 144
  26. def OAI.EilenbergGanea.SeedConnection.Related line 155
  27. theorem OAI.EilenbergGanea.SeedConnection.related_symm line 157
  28. theorem OAI.EilenbergGanea.SeedConnection.related_forward line 162
  29. def OAI.EilenbergGanea.SeedConnection.connection line 171
  30. theorem OAI.EilenbergGanea.SeedConnection.connection_diag line 174
  31. theorem OAI.EilenbergGanea.SeedConnection.connection_reverse line 177
  32. theorem OAI.EilenbergGanea.SeedConnection.connection_flat_sorted line 186
  33. theorem OAI.EilenbergGanea.SeedConnection.connection_flat line 192
  34. def OAI.EilenbergGanea.SeedConnection.rankFin line 232
  35. theorem OAI.EilenbergGanea.SeedConnection.adjacent_rank_ne line 235
  36. theorem OAI.EilenbergGanea.SeedConnection.clique_card_le_three line 241
  37. def OAI.EilenbergGanea.SeedConnection.roseLoop line 251

    Source documentation

    The subdivided x-circle in the exact 103-cell order graph.

    def roseLoop : List SeedCell :=
…

    Mentions: OAI.EilenbergGanea.SeedCell

  38. theorem OAI.EilenbergGanea.SeedConnection.roseLoop_edges line 256
  39. theorem OAI.EilenbergGanea.SeedConnection.roseLoop_holonomy line 259
  40. theorem OAI.EilenbergGanea.SeedConnection.roseLoop_nontrivial line 263