OAI/Geometry/Borsuk/FiniteCases/Cases106.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c31742 line 17
  2. theorem OAI.BorsukNine.FiniteObstruction.c31744 line 26
  3. theorem OAI.BorsukNine.FiniteObstruction.c31745 line 35
  4. theorem OAI.BorsukNine.FiniteObstruction.c31747 line 44
  5. theorem OAI.BorsukNine.FiniteObstruction.c31748 line 53
  6. theorem OAI.BorsukNine.FiniteObstruction.c31750 line 62
  7. theorem OAI.BorsukNine.FiniteObstruction.c31751 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c31752 line 80
  9. theorem OAI.BorsukNine.FiniteObstruction.c31755 line 89
  10. theorem OAI.BorsukNine.FiniteObstruction.c31756 line 98
  11. theorem OAI.BorsukNine.FiniteObstruction.c31757 line 107
  12. theorem OAI.BorsukNine.FiniteObstruction.c31764 line 116
  13. theorem OAI.BorsukNine.FiniteObstruction.c31765 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c31767 line 134
  15. theorem OAI.BorsukNine.FiniteObstruction.c31769 line 143
  16. theorem OAI.BorsukNine.FiniteObstruction.c31777 line 152
  17. theorem OAI.BorsukNine.FiniteObstruction.c31779 line 161
  18. theorem OAI.BorsukNine.FiniteObstruction.c31785 line 170
  19. theorem OAI.BorsukNine.FiniteObstruction.c31787 line 179
  20. theorem OAI.BorsukNine.FiniteObstruction.c31789 line 188
  21. theorem OAI.BorsukNine.FiniteObstruction.c31790 line 197
  22. theorem OAI.BorsukNine.FiniteObstruction.c31797 line 206
  23. theorem OAI.BorsukNine.FiniteObstruction.c31807 line 215
  24. theorem OAI.BorsukNine.FiniteObstruction.c31809 line 224
  25. theorem OAI.BorsukNine.FiniteObstruction.c31810 line 233
  26. theorem OAI.BorsukNine.FiniteObstruction.c31815 line 242
  27. theorem OAI.BorsukNine.FiniteObstruction.c31816 line 251
  28. theorem OAI.BorsukNine.FiniteObstruction.c31817 line 260
  29. theorem OAI.BorsukNine.FiniteObstruction.c31819 line 269
  30. theorem OAI.BorsukNine.FiniteObstruction.c31820 line 278
  31. theorem OAI.BorsukNine.FiniteObstruction.c31837 line 287
  32. theorem OAI.BorsukNine.FiniteObstruction.c31840 line 296
  33. theorem OAI.BorsukNine.FiniteObstruction.c31846 line 305
  34. theorem OAI.BorsukNine.FiniteObstruction.c31847 line 314
  35. theorem OAI.BorsukNine.FiniteObstruction.c31848 line 323
  36. theorem OAI.BorsukNine.FiniteObstruction.c31851 line 332
  37. theorem OAI.BorsukNine.FiniteObstruction.c31853 line 341
  38. theorem OAI.BorsukNine.FiniteObstruction.c31857 line 350
  39. theorem OAI.BorsukNine.FiniteObstruction.c31869 line 359
  40. theorem OAI.BorsukNine.FiniteObstruction.c31877 line 368
  41. theorem OAI.BorsukNine.FiniteObstruction.c31880 line 377
  42. theorem OAI.BorsukNine.FiniteObstruction.c31881 line 386
  43. theorem OAI.BorsukNine.FiniteObstruction.c31884 line 395
  44. theorem OAI.BorsukNine.FiniteObstruction.c31885 line 404
  45. theorem OAI.BorsukNine.FiniteObstruction.c31886 line 413
  46. theorem OAI.BorsukNine.FiniteObstruction.c31887 line 422
  47. theorem OAI.BorsukNine.FiniteObstruction.c31897 line 431