OAI/Geometry/Borsuk/FiniteCases/Cases073.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c28527 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c28528 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c28530 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c28535 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c28543 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c28544 line 59
  7. theorem OAI.BorsukNine.FiniteObstruction.c28550 line 67
  8. theorem OAI.BorsukNine.FiniteObstruction.c28555 line 75
  9. theorem OAI.BorsukNine.FiniteObstruction.c28558 line 83
  10. theorem OAI.BorsukNine.FiniteObstruction.c28560 line 91
  11. theorem OAI.BorsukNine.FiniteObstruction.c28561 line 99
  12. theorem OAI.BorsukNine.FiniteObstruction.c28603 line 107
  13. theorem OAI.BorsukNine.FiniteObstruction.c28605 line 117
  14. theorem OAI.BorsukNine.FiniteObstruction.c28607 line 127
  15. theorem OAI.BorsukNine.FiniteObstruction.c28618 line 137
  16. theorem OAI.BorsukNine.FiniteObstruction.c28619 line 147
  17. theorem OAI.BorsukNine.FiniteObstruction.c28655 line 157
  18. theorem OAI.BorsukNine.FiniteObstruction.c28662 line 167
  19. theorem OAI.BorsukNine.FiniteObstruction.c28664 line 177
  20. theorem OAI.BorsukNine.FiniteObstruction.c28667 line 187
  21. theorem OAI.BorsukNine.FiniteObstruction.c28678 line 197
  22. theorem OAI.BorsukNine.FiniteObstruction.c28680 line 207
  23. theorem OAI.BorsukNine.FiniteObstruction.c28683 line 217
  24. theorem OAI.BorsukNine.FiniteObstruction.c28685 line 225
  25. theorem OAI.BorsukNine.FiniteObstruction.c28686 line 233
  26. theorem OAI.BorsukNine.FiniteObstruction.c28688 line 241
  27. theorem OAI.BorsukNine.FiniteObstruction.c28689 line 249
  28. theorem OAI.BorsukNine.FiniteObstruction.c28690 line 257
  29. theorem OAI.BorsukNine.FiniteObstruction.c28691 line 265
  30. theorem OAI.BorsukNine.FiniteObstruction.c28694 line 273
  31. theorem OAI.BorsukNine.FiniteObstruction.c28695 line 281
  32. theorem OAI.BorsukNine.FiniteObstruction.c28696 line 289
  33. theorem OAI.BorsukNine.FiniteObstruction.c28697 line 297
  34. theorem OAI.BorsukNine.FiniteObstruction.c28698 line 305
  35. theorem OAI.BorsukNine.FiniteObstruction.c28700 line 313
  36. theorem OAI.BorsukNine.FiniteObstruction.c28701 line 321
  37. theorem OAI.BorsukNine.FiniteObstruction.c28705 line 329
  38. theorem OAI.BorsukNine.FiniteObstruction.c28707 line 339
  39. theorem OAI.BorsukNine.FiniteObstruction.c28715 line 349
  40. theorem OAI.BorsukNine.FiniteObstruction.c28738 line 359
  41. theorem OAI.BorsukNine.FiniteObstruction.c28743 line 369
  42. theorem OAI.BorsukNine.FiniteObstruction.c28745 line 379
  43. theorem OAI.BorsukNine.FiniteObstruction.c28747 line 389
  44. theorem OAI.BorsukNine.FiniteObstruction.c28748 line 399
  45. theorem OAI.BorsukNine.FiniteObstruction.c28753 line 409
  46. theorem OAI.BorsukNine.FiniteObstruction.c28759 line 419
  47. theorem OAI.BorsukNine.FiniteObstruction.c28766 line 429