OAI/Geometry/Borsuk/FiniteCases/Cases053.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c18472 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c18474 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c18476 line 27
  4. theorem OAI.BorsukNine.FiniteObstruction.c18477 line 35
  5. theorem OAI.BorsukNine.FiniteObstruction.c18478 line 43
  6. theorem OAI.BorsukNine.FiniteObstruction.c18479 line 51
  7. theorem OAI.BorsukNine.FiniteObstruction.c18481 line 59
  8. theorem OAI.BorsukNine.FiniteObstruction.c18485 line 67
  9. theorem OAI.BorsukNine.FiniteObstruction.c18487 line 77
  10. theorem OAI.BorsukNine.FiniteObstruction.c18488 line 87
  11. theorem OAI.BorsukNine.FiniteObstruction.c18489 line 97
  12. theorem OAI.BorsukNine.FiniteObstruction.c18500 line 107
  13. theorem OAI.BorsukNine.FiniteObstruction.c18530 line 117
  14. theorem OAI.BorsukNine.FiniteObstruction.c18531 line 127
  15. theorem OAI.BorsukNine.FiniteObstruction.c18533 line 137
  16. theorem OAI.BorsukNine.FiniteObstruction.c18537 line 147
  17. theorem OAI.BorsukNine.FiniteObstruction.c18540 line 157
  18. theorem OAI.BorsukNine.FiniteObstruction.c18548 line 167
  19. theorem OAI.BorsukNine.FiniteObstruction.c18549 line 177
  20. theorem OAI.BorsukNine.FiniteObstruction.c18551 line 187
  21. theorem OAI.BorsukNine.FiniteObstruction.c18554 line 197
  22. theorem OAI.BorsukNine.FiniteObstruction.c18555 line 207
  23. theorem OAI.BorsukNine.FiniteObstruction.c18556 line 217
  24. theorem OAI.BorsukNine.FiniteObstruction.c18558 line 227
  25. theorem OAI.BorsukNine.FiniteObstruction.c18559 line 237
  26. theorem OAI.BorsukNine.FiniteObstruction.c18561 line 247
  27. theorem OAI.BorsukNine.FiniteObstruction.c18565 line 257
  28. theorem OAI.BorsukNine.FiniteObstruction.c18567 line 267
  29. theorem OAI.BorsukNine.FiniteObstruction.c18568 line 277
  30. theorem OAI.BorsukNine.FiniteObstruction.c18584 line 287
  31. theorem OAI.BorsukNine.FiniteObstruction.c18603 line 297
  32. theorem OAI.BorsukNine.FiniteObstruction.c18604 line 305
  33. theorem OAI.BorsukNine.FiniteObstruction.c18605 line 313
  34. theorem OAI.BorsukNine.FiniteObstruction.c18612 line 321
  35. theorem OAI.BorsukNine.FiniteObstruction.c18614 line 329
  36. theorem OAI.BorsukNine.FiniteObstruction.c18618 line 337
  37. theorem OAI.BorsukNine.FiniteObstruction.c18621 line 345
  38. theorem OAI.BorsukNine.FiniteObstruction.c18631 line 353
  39. theorem OAI.BorsukNine.FiniteObstruction.c18655 line 363
  40. theorem OAI.BorsukNine.FiniteObstruction.c18667 line 373
  41. theorem OAI.BorsukNine.FiniteObstruction.c18715 line 383
  42. theorem OAI.BorsukNine.FiniteObstruction.c18727 line 393
  43. theorem OAI.BorsukNine.FiniteObstruction.c18743 line 403
  44. theorem OAI.BorsukNine.FiniteObstruction.c18757 line 411
  45. theorem OAI.BorsukNine.FiniteObstruction.c18765 line 419
  46. theorem OAI.BorsukNine.FiniteObstruction.c18767 line 429