OAI/Algebra/GroupRing/ConeCells.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.cons_tail_time line 14
  2. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.cylinder_side line 21
  3. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.cylinder_bottom line 34
  4. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.cylinder_top line 43
  5. def OAI.TorsionFreeZeroDivisors.GraphConeCW.endpoint line 55
  6. def OAI.TorsionFreeZeroDivisors.GraphConeCW.oneBoundary line 60
  7. abbrev OAI.TorsionFreeZeroDivisors.GraphConeCW.One line 62
  8. def OAI.TorsionFreeZeroDivisors.GraphConeCW.vertex line 63
  9. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.minus_ne_plus line 64
  10. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.oneBoundary_minus line 68
  11. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.oneBoundary_plus line 70
  12. def OAI.TorsionFreeZeroDivisors.GraphConeCW.radial line 72
  13. def OAI.TorsionFreeZeroDivisors.GraphConeCW.outer line 73
  14. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.radial_zero line 74
  15. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.radial_one line 78
  16. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.outer_minus line 82
  17. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.outer_plus line 86
  18. def OAI.TorsionFreeZeroDivisors.GraphConeCW.sides line 90
  19. def OAI.TorsionFreeZeroDivisors.GraphConeCW.ends line 92
  20. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.compatible line 94
  21. def OAI.TorsionFreeZeroDivisors.GraphConeCW.twoBoundary line 97
  22. abbrev OAI.TorsionFreeZeroDivisors.GraphConeCW.Cone line 98
  23. def OAI.TorsionFreeZeroDivisors.GraphConeCW.inclusion line 99
  24. def OAI.TorsionFreeZeroDivisors.GraphConeCW.apex line 100
  25. def OAI.TorsionFreeZeroDivisors.GraphConeCW.square line 101
  26. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.square_side line 102
  27. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.square_bottom line 107
  28. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.square_top line 112
  29. def OAI.TorsionFreeZeroDivisors.GraphConeCW.joinTime line 116
  30. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.continuous_joinTime line 120
  31. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.joinTime_zero line 123
  32. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.joinTime_one line 124
  33. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.zero_joinTime line 125
  34. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.one_joinTime line 126
  35. def OAI.TorsionFreeZeroDivisors.GraphConeCW.vertexPaths line 127
  36. def OAI.TorsionFreeZeroDivisors.GraphConeCW.radialPaths line 131
  37. def OAI.TorsionFreeZeroDivisors.GraphConeCW.outerPaths line 136
  38. def OAI.TorsionFreeZeroDivisors.GraphConeCW.edgePaths line 138
  39. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.edgePaths_boundary line 139
  40. def OAI.TorsionFreeZeroDivisors.GraphConeCW.onePaths line 154
  41. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.onePaths_vertex line 156
  42. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.onePaths_outer line 157
  43. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.onePaths_radial line 162
  44. def OAI.TorsionFreeZeroDivisors.GraphConeCW.squarePaths line 168
  45. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.squarePaths_boundary line 173
  46. def OAI.TorsionFreeZeroDivisors.GraphConeCW.contractionPaths line 198
  47. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.onePaths_zero line 200
  48. lemma OAI.TorsionFreeZeroDivisors.GraphConeCW.onePaths_one line 216
  49. def OAI.TorsionFreeZeroDivisors.GraphConeCW.contraction line 230
  50. instance OAI.TorsionFreeZeroDivisors.GraphConeCW.contractible line 253