OAI/Geometry/Borsuk/FiniteCases/Cases042.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c12596 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c12597 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c12605 line 27
  4. theorem OAI.BorsukNine.FiniteObstruction.c12607 line 37
  5. theorem OAI.BorsukNine.FiniteObstruction.c12613 line 47
  6. theorem OAI.BorsukNine.FiniteObstruction.c12615 line 57
  7. theorem OAI.BorsukNine.FiniteObstruction.c12616 line 67
  8. theorem OAI.BorsukNine.FiniteObstruction.c12634 line 77
  9. theorem OAI.BorsukNine.FiniteObstruction.c12635 line 87
  10. theorem OAI.BorsukNine.FiniteObstruction.c12636 line 97
  11. theorem OAI.BorsukNine.FiniteObstruction.c12645 line 107
  12. theorem OAI.BorsukNine.FiniteObstruction.c12647 line 117
  13. theorem OAI.BorsukNine.FiniteObstruction.c12657 line 127
  14. theorem OAI.BorsukNine.FiniteObstruction.c12663 line 137
  15. theorem OAI.BorsukNine.FiniteObstruction.c12682 line 147
  16. theorem OAI.BorsukNine.FiniteObstruction.c12684 line 157
  17. theorem OAI.BorsukNine.FiniteObstruction.c12690 line 167
  18. theorem OAI.BorsukNine.FiniteObstruction.c12691 line 177
  19. theorem OAI.BorsukNine.FiniteObstruction.c12695 line 187
  20. theorem OAI.BorsukNine.FiniteObstruction.c12699 line 197
  21. theorem OAI.BorsukNine.FiniteObstruction.c12707 line 207
  22. theorem OAI.BorsukNine.FiniteObstruction.c12710 line 217
  23. theorem OAI.BorsukNine.FiniteObstruction.c12716 line 227
  24. theorem OAI.BorsukNine.FiniteObstruction.c12723 line 237
  25. theorem OAI.BorsukNine.FiniteObstruction.c12726 line 245
  26. theorem OAI.BorsukNine.FiniteObstruction.c12735 line 253
  27. theorem OAI.BorsukNine.FiniteObstruction.c12736 line 261
  28. theorem OAI.BorsukNine.FiniteObstruction.c12751 line 269
  29. theorem OAI.BorsukNine.FiniteObstruction.c12863 line 279
  30. theorem OAI.BorsukNine.FiniteObstruction.c12864 line 287
  31. theorem OAI.BorsukNine.FiniteObstruction.c12866 line 295
  32. theorem OAI.BorsukNine.FiniteObstruction.c12867 line 303
  33. theorem OAI.BorsukNine.FiniteObstruction.c12868 line 311
  34. theorem OAI.BorsukNine.FiniteObstruction.c12869 line 319
  35. theorem OAI.BorsukNine.FiniteObstruction.c12871 line 327
  36. theorem OAI.BorsukNine.FiniteObstruction.c12872 line 335
  37. theorem OAI.BorsukNine.FiniteObstruction.c12874 line 343
  38. theorem OAI.BorsukNine.FiniteObstruction.c12875 line 351
  39. theorem OAI.BorsukNine.FiniteObstruction.c12877 line 359
  40. theorem OAI.BorsukNine.FiniteObstruction.c12878 line 367
  41. theorem OAI.BorsukNine.FiniteObstruction.c12881 line 375
  42. theorem OAI.BorsukNine.FiniteObstruction.c12883 line 383
  43. theorem OAI.BorsukNine.FiniteObstruction.c12885 line 393
  44. theorem OAI.BorsukNine.FiniteObstruction.c12887 line 403
  45. theorem OAI.BorsukNine.FiniteObstruction.c12888 line 413
  46. theorem OAI.BorsukNine.FiniteObstruction.c12891 line 423