OAI/Geometry/Borsuk/FiniteCases/Cases001.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c3 line 10
  2. theorem OAI.BorsukNine.FiniteObstruction.c4 line 15
  3. theorem OAI.BorsukNine.FiniteObstruction.c18 line 32
  4. theorem OAI.BorsukNine.FiniteObstruction.c19 line 37
  5. theorem OAI.BorsukNine.FiniteObstruction.c33 line 54
  6. theorem OAI.BorsukNine.FiniteObstruction.c35 line 59
  7. theorem OAI.BorsukNine.FiniteObstruction.c39 line 64
  8. theorem OAI.BorsukNine.FiniteObstruction.c40 line 69
  9. theorem OAI.BorsukNine.FiniteObstruction.c41 line 86
  10. theorem OAI.BorsukNine.FiniteObstruction.c48 line 91
  11. theorem OAI.BorsukNine.FiniteObstruction.c50 line 96
  12. theorem OAI.BorsukNine.FiniteObstruction.c52 line 101
  13. theorem OAI.BorsukNine.FiniteObstruction.c54 line 106
  14. theorem OAI.BorsukNine.FiniteObstruction.c56 line 111
  15. theorem OAI.BorsukNine.FiniteObstruction.c58 line 116
  16. theorem OAI.BorsukNine.FiniteObstruction.c60 line 121
  17. theorem OAI.BorsukNine.FiniteObstruction.c62 line 126
  18. theorem OAI.BorsukNine.FiniteObstruction.c63 line 143
  19. theorem OAI.BorsukNine.FiniteObstruction.c65 line 148
  20. theorem OAI.BorsukNine.FiniteObstruction.c66 line 153
  21. theorem OAI.BorsukNine.FiniteObstruction.c67 line 170
  22. theorem OAI.BorsukNine.FiniteObstruction.c68 line 175
  23. theorem OAI.BorsukNine.FiniteObstruction.c69 line 192
  24. theorem OAI.BorsukNine.FiniteObstruction.c73 line 197
  25. theorem OAI.BorsukNine.FiniteObstruction.c76 line 202
  26. theorem OAI.BorsukNine.FiniteObstruction.c78 line 219
  27. theorem OAI.BorsukNine.FiniteObstruction.c80 line 224
  28. theorem OAI.BorsukNine.FiniteObstruction.c81 line 229
  29. theorem OAI.BorsukNine.FiniteObstruction.c82 line 246
  30. theorem OAI.BorsukNine.FiniteObstruction.c84 line 251
  31. theorem OAI.BorsukNine.FiniteObstruction.c95 line 256
  32. theorem OAI.BorsukNine.FiniteObstruction.c97 line 261
  33. theorem OAI.BorsukNine.FiniteObstruction.c99 line 266
  34. theorem OAI.BorsukNine.FiniteObstruction.c105 line 271
  35. theorem OAI.BorsukNine.FiniteObstruction.c107 line 276
  36. theorem OAI.BorsukNine.FiniteObstruction.c108 line 293
  37. theorem OAI.BorsukNine.FiniteObstruction.c110 line 298
  38. theorem OAI.BorsukNine.FiniteObstruction.c113 line 303
  39. theorem OAI.BorsukNine.FiniteObstruction.c119 line 320
  40. theorem OAI.BorsukNine.FiniteObstruction.c123 line 337
  41. theorem OAI.BorsukNine.FiniteObstruction.c124 line 342
  42. theorem OAI.BorsukNine.FiniteObstruction.c137 line 359
  43. theorem OAI.BorsukNine.FiniteObstruction.c138 line 376
  44. theorem OAI.BorsukNine.FiniteObstruction.c140 line 381
  45. theorem OAI.BorsukNine.FiniteObstruction.c141 line 386
  46. theorem OAI.BorsukNine.FiniteObstruction.c142 line 403
  47. theorem OAI.BorsukNine.FiniteObstruction.c144 line 408
  48. theorem OAI.BorsukNine.FiniteObstruction.c146 line 413
  49. theorem OAI.BorsukNine.FiniteObstruction.c148 line 418
  50. theorem OAI.BorsukNine.FiniteObstruction.c150 line 423
  51. theorem OAI.BorsukNine.FiniteObstruction.c152 line 428