OAI/Geometry/Borsuk/FiniteCases/Cases059.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c21327 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c21332 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c21337 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c21387 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c21404 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c21405 line 59
  7. theorem OAI.BorsukNine.FiniteObstruction.c21408 line 67
  8. theorem OAI.BorsukNine.FiniteObstruction.c21523 line 75
  9. theorem OAI.BorsukNine.FiniteObstruction.c21543 line 85
  10. theorem OAI.BorsukNine.FiniteObstruction.c21544 line 93
  11. theorem OAI.BorsukNine.FiniteObstruction.c21545 line 101
  12. theorem OAI.BorsukNine.FiniteObstruction.c21551 line 109
  13. theorem OAI.BorsukNine.FiniteObstruction.c21553 line 117
  14. theorem OAI.BorsukNine.FiniteObstruction.c21644 line 125
  15. theorem OAI.BorsukNine.FiniteObstruction.c21645 line 135
  16. theorem OAI.BorsukNine.FiniteObstruction.c21646 line 145
  17. theorem OAI.BorsukNine.FiniteObstruction.c21657 line 155
  18. theorem OAI.BorsukNine.FiniteObstruction.c21681 line 165
  19. theorem OAI.BorsukNine.FiniteObstruction.c21682 line 175
  20. theorem OAI.BorsukNine.FiniteObstruction.c21684 line 183
  21. theorem OAI.BorsukNine.FiniteObstruction.c21699 line 191
  22. theorem OAI.BorsukNine.FiniteObstruction.c21737 line 199
  23. theorem OAI.BorsukNine.FiniteObstruction.c21785 line 209
  24. theorem OAI.BorsukNine.FiniteObstruction.c21786 line 219
  25. theorem OAI.BorsukNine.FiniteObstruction.c21787 line 229
  26. theorem OAI.BorsukNine.FiniteObstruction.c21821 line 239
  27. theorem OAI.BorsukNine.FiniteObstruction.c21822 line 249
  28. theorem OAI.BorsukNine.FiniteObstruction.c21824 line 257
  29. theorem OAI.BorsukNine.FiniteObstruction.c21827 line 265
  30. theorem OAI.BorsukNine.FiniteObstruction.c21828 line 273
  31. theorem OAI.BorsukNine.FiniteObstruction.c21842 line 281
  32. theorem OAI.BorsukNine.FiniteObstruction.c21937 line 291
  33. theorem OAI.BorsukNine.FiniteObstruction.c21945 line 301
  34. theorem OAI.BorsukNine.FiniteObstruction.c21962 line 311
  35. theorem OAI.BorsukNine.FiniteObstruction.c21964 line 319
  36. theorem OAI.BorsukNine.FiniteObstruction.c21965 line 327
  37. theorem OAI.BorsukNine.FiniteObstruction.c21967 line 335
  38. theorem OAI.BorsukNine.FiniteObstruction.c21975 line 343
  39. theorem OAI.BorsukNine.FiniteObstruction.c21981 line 351
  40. theorem OAI.BorsukNine.FiniteObstruction.c21982 line 359
  41. theorem OAI.BorsukNine.FiniteObstruction.c22005 line 369
  42. theorem OAI.BorsukNine.FiniteObstruction.c22034 line 379
  43. theorem OAI.BorsukNine.FiniteObstruction.c22045 line 389
  44. theorem OAI.BorsukNine.FiniteObstruction.c22074 line 399
  45. theorem OAI.BorsukNine.FiniteObstruction.c22075 line 409
  46. theorem OAI.BorsukNine.FiniteObstruction.c22076 line 419
  47. theorem OAI.BorsukNine.FiniteObstruction.c22083 line 429