OAI/Geometry/Borsuk/FiniteCases/Cases040.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c11875 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c11880 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c11883 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c11886 line 39
  5. theorem OAI.BorsukNine.FiniteObstruction.c11890 line 47
  6. theorem OAI.BorsukNine.FiniteObstruction.c11892 line 55
  7. theorem OAI.BorsukNine.FiniteObstruction.c11893 line 63
  8. theorem OAI.BorsukNine.FiniteObstruction.c11894 line 71
  9. theorem OAI.BorsukNine.FiniteObstruction.c11898 line 79
  10. theorem OAI.BorsukNine.FiniteObstruction.c11899 line 87
  11. theorem OAI.BorsukNine.FiniteObstruction.c11903 line 95
  12. theorem OAI.BorsukNine.FiniteObstruction.c11911 line 105
  13. theorem OAI.BorsukNine.FiniteObstruction.c11915 line 115
  14. theorem OAI.BorsukNine.FiniteObstruction.c11930 line 125
  15. theorem OAI.BorsukNine.FiniteObstruction.c11932 line 135
  16. theorem OAI.BorsukNine.FiniteObstruction.c11933 line 145
  17. theorem OAI.BorsukNine.FiniteObstruction.c11963 line 155
  18. theorem OAI.BorsukNine.FiniteObstruction.c11982 line 165
  19. theorem OAI.BorsukNine.FiniteObstruction.c11984 line 175
  20. theorem OAI.BorsukNine.FiniteObstruction.c12007 line 185
  21. theorem OAI.BorsukNine.FiniteObstruction.c12010 line 195
  22. theorem OAI.BorsukNine.FiniteObstruction.c12012 line 205
  23. theorem OAI.BorsukNine.FiniteObstruction.c12023 line 215
  24. theorem OAI.BorsukNine.FiniteObstruction.c12026 line 223
  25. theorem OAI.BorsukNine.FiniteObstruction.c12031 line 231
  26. theorem OAI.BorsukNine.FiniteObstruction.c12033 line 239
  27. theorem OAI.BorsukNine.FiniteObstruction.c12035 line 247
  28. theorem OAI.BorsukNine.FiniteObstruction.c12051 line 255
  29. theorem OAI.BorsukNine.FiniteObstruction.c12053 line 265
  30. theorem OAI.BorsukNine.FiniteObstruction.c12055 line 275
  31. theorem OAI.BorsukNine.FiniteObstruction.c12092 line 285
  32. theorem OAI.BorsukNine.FiniteObstruction.c12103 line 295
  33. theorem OAI.BorsukNine.FiniteObstruction.c12108 line 305
  34. theorem OAI.BorsukNine.FiniteObstruction.c12139 line 315
  35. theorem OAI.BorsukNine.FiniteObstruction.c12163 line 325
  36. theorem OAI.BorsukNine.FiniteObstruction.c12185 line 333
  37. theorem OAI.BorsukNine.FiniteObstruction.c12193 line 343
  38. theorem OAI.BorsukNine.FiniteObstruction.c12195 line 353
  39. theorem OAI.BorsukNine.FiniteObstruction.c12217 line 363
  40. theorem OAI.BorsukNine.FiniteObstruction.c12249 line 373
  41. theorem OAI.BorsukNine.FiniteObstruction.c12270 line 383
  42. theorem OAI.BorsukNine.FiniteObstruction.c12303 line 393
  43. theorem OAI.BorsukNine.FiniteObstruction.c12305 line 401
  44. theorem OAI.BorsukNine.FiniteObstruction.c12306 line 409
  45. theorem OAI.BorsukNine.FiniteObstruction.c12309 line 417
  46. theorem OAI.BorsukNine.FiniteObstruction.c12310 line 425