OAI/Geometry/Borsuk/FiniteCases/Cases033.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c7879 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c7910 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c7933 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c7945 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c7954 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c7955 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c7956 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c7964 line 81
  9. theorem OAI.BorsukNine.FiniteObstruction.c7968 line 89
  10. theorem OAI.BorsukNine.FiniteObstruction.c7969 line 97
  11. theorem OAI.BorsukNine.FiniteObstruction.c7979 line 105
  12. theorem OAI.BorsukNine.FiniteObstruction.c8057 line 113
  13. theorem OAI.BorsukNine.FiniteObstruction.c8065 line 123
  14. theorem OAI.BorsukNine.FiniteObstruction.c8073 line 133
  15. theorem OAI.BorsukNine.FiniteObstruction.c8089 line 143
  16. theorem OAI.BorsukNine.FiniteObstruction.c8095 line 153
  17. theorem OAI.BorsukNine.FiniteObstruction.c8103 line 163
  18. theorem OAI.BorsukNine.FiniteObstruction.c8111 line 171
  19. theorem OAI.BorsukNine.FiniteObstruction.c8113 line 179
  20. theorem OAI.BorsukNine.FiniteObstruction.c8119 line 187
  21. theorem OAI.BorsukNine.FiniteObstruction.c8177 line 195
  22. theorem OAI.BorsukNine.FiniteObstruction.c8205 line 205
  23. theorem OAI.BorsukNine.FiniteObstruction.c8207 line 215
  24. theorem OAI.BorsukNine.FiniteObstruction.c8228 line 225
  25. theorem OAI.BorsukNine.FiniteObstruction.c8230 line 235
  26. theorem OAI.BorsukNine.FiniteObstruction.c8232 line 245
  27. theorem OAI.BorsukNine.FiniteObstruction.c8233 line 255
  28. theorem OAI.BorsukNine.FiniteObstruction.c8236 line 265
  29. theorem OAI.BorsukNine.FiniteObstruction.c8248 line 275
  30. theorem OAI.BorsukNine.FiniteObstruction.c8267 line 283
  31. theorem OAI.BorsukNine.FiniteObstruction.c8275 line 293
  32. theorem OAI.BorsukNine.FiniteObstruction.c8289 line 303
  33. theorem OAI.BorsukNine.FiniteObstruction.c8335 line 313
  34. theorem OAI.BorsukNine.FiniteObstruction.c8342 line 323
  35. theorem OAI.BorsukNine.FiniteObstruction.c8345 line 333
  36. theorem OAI.BorsukNine.FiniteObstruction.c8351 line 343
  37. theorem OAI.BorsukNine.FiniteObstruction.c8386 line 353
  38. theorem OAI.BorsukNine.FiniteObstruction.c8393 line 361
  39. theorem OAI.BorsukNine.FiniteObstruction.c8403 line 369
  40. theorem OAI.BorsukNine.FiniteObstruction.c8475 line 379
  41. theorem OAI.BorsukNine.FiniteObstruction.c8482 line 389
  42. theorem OAI.BorsukNine.FiniteObstruction.c8485 line 399
  43. theorem OAI.BorsukNine.FiniteObstruction.c8487 line 409
  44. theorem OAI.BorsukNine.FiniteObstruction.c8508 line 419
  45. theorem OAI.BorsukNine.FiniteObstruction.c8509 line 429