OAI/Geometry/Borsuk/FiniteCases/Cases025.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c2657 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c2661 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c2665 line 27
  4. theorem OAI.BorsukNine.FiniteObstruction.c2673 line 37
  5. theorem OAI.BorsukNine.FiniteObstruction.c2678 line 47
  6. theorem OAI.BorsukNine.FiniteObstruction.c2691 line 57
  7. theorem OAI.BorsukNine.FiniteObstruction.c2703 line 67
  8. theorem OAI.BorsukNine.FiniteObstruction.c2747 line 77
  9. theorem OAI.BorsukNine.FiniteObstruction.c2753 line 87
  10. theorem OAI.BorsukNine.FiniteObstruction.c2754 line 97
  11. theorem OAI.BorsukNine.FiniteObstruction.c2763 line 107
  12. theorem OAI.BorsukNine.FiniteObstruction.c2789 line 117
  13. theorem OAI.BorsukNine.FiniteObstruction.c2790 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c2791 line 133
  15. theorem OAI.BorsukNine.FiniteObstruction.c2795 line 141
  16. theorem OAI.BorsukNine.FiniteObstruction.c2811 line 149
  17. theorem OAI.BorsukNine.FiniteObstruction.c2861 line 159
  18. theorem OAI.BorsukNine.FiniteObstruction.c2927 line 169
  19. theorem OAI.BorsukNine.FiniteObstruction.c2936 line 177
  20. theorem OAI.BorsukNine.FiniteObstruction.c2992 line 185
  21. theorem OAI.BorsukNine.FiniteObstruction.c3011 line 195
  22. theorem OAI.BorsukNine.FiniteObstruction.c3035 line 205
  23. theorem OAI.BorsukNine.FiniteObstruction.c3062 line 215
  24. theorem OAI.BorsukNine.FiniteObstruction.c3063 line 223
  25. theorem OAI.BorsukNine.FiniteObstruction.c3064 line 231
  26. theorem OAI.BorsukNine.FiniteObstruction.c3066 line 239
  27. theorem OAI.BorsukNine.FiniteObstruction.c3068 line 247
  28. theorem OAI.BorsukNine.FiniteObstruction.c3072 line 255
  29. theorem OAI.BorsukNine.FiniteObstruction.c3073 line 263
  30. theorem OAI.BorsukNine.FiniteObstruction.c3075 line 271
  31. theorem OAI.BorsukNine.FiniteObstruction.c3081 line 279
  32. theorem OAI.BorsukNine.FiniteObstruction.c3180 line 287
  33. theorem OAI.BorsukNine.FiniteObstruction.c3203 line 297
  34. theorem OAI.BorsukNine.FiniteObstruction.c3205 line 305
  35. theorem OAI.BorsukNine.FiniteObstruction.c3212 line 313
  36. theorem OAI.BorsukNine.FiniteObstruction.c3219 line 321
  37. theorem OAI.BorsukNine.FiniteObstruction.c3221 line 329
  38. theorem OAI.BorsukNine.FiniteObstruction.c3231 line 337
  39. theorem OAI.BorsukNine.FiniteObstruction.c3295 line 347
  40. theorem OAI.BorsukNine.FiniteObstruction.c3297 line 357
  41. theorem OAI.BorsukNine.FiniteObstruction.c3304 line 367
  42. theorem OAI.BorsukNine.FiniteObstruction.c3305 line 377
  43. theorem OAI.BorsukNine.FiniteObstruction.c3307 line 387
  44. theorem OAI.BorsukNine.FiniteObstruction.c3343 line 397
  45. theorem OAI.BorsukNine.FiniteObstruction.c3351 line 405
  46. theorem OAI.BorsukNine.FiniteObstruction.c3363 line 413
  47. theorem OAI.BorsukNine.FiniteObstruction.c3371 line 423