OAI/Geometry/Borsuk/FiniteCases/Cases009.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c733 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c734 line 16
  3. theorem OAI.BorsukNine.FiniteObstruction.c735 line 33
  4. theorem OAI.BorsukNine.FiniteObstruction.c736 line 38
  5. theorem OAI.BorsukNine.FiniteObstruction.c737 line 55
  6. theorem OAI.BorsukNine.FiniteObstruction.c742 line 72
  7. theorem OAI.BorsukNine.FiniteObstruction.c744 line 77
  8. theorem OAI.BorsukNine.FiniteObstruction.c746 line 82
  9. theorem OAI.BorsukNine.FiniteObstruction.c747 line 87
  10. theorem OAI.BorsukNine.FiniteObstruction.c748 line 104
  11. theorem OAI.BorsukNine.FiniteObstruction.c749 line 109
  12. theorem OAI.BorsukNine.FiniteObstruction.c752 line 126
  13. theorem OAI.BorsukNine.FiniteObstruction.c757 line 143
  14. theorem OAI.BorsukNine.FiniteObstruction.c759 line 148
  15. theorem OAI.BorsukNine.FiniteObstruction.c761 line 153
  16. theorem OAI.BorsukNine.FiniteObstruction.c763 line 158
  17. theorem OAI.BorsukNine.FiniteObstruction.c765 line 163
  18. theorem OAI.BorsukNine.FiniteObstruction.c766 line 168
  19. theorem OAI.BorsukNine.FiniteObstruction.c768 line 185
  20. theorem OAI.BorsukNine.FiniteObstruction.c772 line 190
  21. theorem OAI.BorsukNine.FiniteObstruction.c774 line 195
  22. theorem OAI.BorsukNine.FiniteObstruction.c775 line 200
  23. theorem OAI.BorsukNine.FiniteObstruction.c776 line 217
  24. theorem OAI.BorsukNine.FiniteObstruction.c780 line 222
  25. theorem OAI.BorsukNine.FiniteObstruction.c789 line 227
  26. theorem OAI.BorsukNine.FiniteObstruction.c797 line 232
  27. theorem OAI.BorsukNine.FiniteObstruction.c802 line 249
  28. theorem OAI.BorsukNine.FiniteObstruction.c806 line 254
  29. theorem OAI.BorsukNine.FiniteObstruction.c808 line 259
  30. theorem OAI.BorsukNine.FiniteObstruction.c810 line 264
  31. theorem OAI.BorsukNine.FiniteObstruction.c812 line 269
  32. theorem OAI.BorsukNine.FiniteObstruction.c814 line 286
  33. theorem OAI.BorsukNine.FiniteObstruction.c817 line 303
  34. theorem OAI.BorsukNine.FiniteObstruction.c819 line 308
  35. theorem OAI.BorsukNine.FiniteObstruction.c823 line 313
  36. theorem OAI.BorsukNine.FiniteObstruction.c824 line 318
  37. theorem OAI.BorsukNine.FiniteObstruction.c826 line 335
  38. theorem OAI.BorsukNine.FiniteObstruction.c827 line 352
  39. theorem OAI.BorsukNine.FiniteObstruction.c829 line 369
  40. theorem OAI.BorsukNine.FiniteObstruction.c831 line 386
  41. theorem OAI.BorsukNine.FiniteObstruction.c832 line 403
  42. theorem OAI.BorsukNine.FiniteObstruction.c835 line 408
  43. theorem OAI.BorsukNine.FiniteObstruction.c836 line 425