OAI/Geometry/Borsuk/FiniteCases/Cases036.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c9739 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c9741 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c9742 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c9745 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c9746 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c9755 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c9763 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c9773 line 81
  9. theorem OAI.BorsukNine.FiniteObstruction.c9779 line 91
  10. theorem OAI.BorsukNine.FiniteObstruction.c9782 line 101
  11. theorem OAI.BorsukNine.FiniteObstruction.c9784 line 109
  12. theorem OAI.BorsukNine.FiniteObstruction.c9788 line 117
  13. theorem OAI.BorsukNine.FiniteObstruction.c9793 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c9801 line 133
  15. theorem OAI.BorsukNine.FiniteObstruction.c9875 line 141
  16. theorem OAI.BorsukNine.FiniteObstruction.c9922 line 151
  17. theorem OAI.BorsukNine.FiniteObstruction.c9923 line 159
  18. theorem OAI.BorsukNine.FiniteObstruction.c9924 line 167
  19. theorem OAI.BorsukNine.FiniteObstruction.c9928 line 175
  20. theorem OAI.BorsukNine.FiniteObstruction.c9929 line 183
  21. theorem OAI.BorsukNine.FiniteObstruction.c9937 line 191
  22. theorem OAI.BorsukNine.FiniteObstruction.c9979 line 199
  23. theorem OAI.BorsukNine.FiniteObstruction.c10011 line 209
  24. theorem OAI.BorsukNine.FiniteObstruction.c10020 line 219
  25. theorem OAI.BorsukNine.FiniteObstruction.c10035 line 229
  26. theorem OAI.BorsukNine.FiniteObstruction.c10039 line 239
  27. theorem OAI.BorsukNine.FiniteObstruction.c10042 line 249
  28. theorem OAI.BorsukNine.FiniteObstruction.c10062 line 259
  29. theorem OAI.BorsukNine.FiniteObstruction.c10064 line 267
  30. theorem OAI.BorsukNine.FiniteObstruction.c10067 line 275
  31. theorem OAI.BorsukNine.FiniteObstruction.c10081 line 283
  32. theorem OAI.BorsukNine.FiniteObstruction.c10155 line 291
  33. theorem OAI.BorsukNine.FiniteObstruction.c10165 line 301
  34. theorem OAI.BorsukNine.FiniteObstruction.c10184 line 311
  35. theorem OAI.BorsukNine.FiniteObstruction.c10202 line 321
  36. theorem OAI.BorsukNine.FiniteObstruction.c10203 line 329
  37. theorem OAI.BorsukNine.FiniteObstruction.c10204 line 337
  38. theorem OAI.BorsukNine.FiniteObstruction.c10206 line 345
  39. theorem OAI.BorsukNine.FiniteObstruction.c10207 line 353
  40. theorem OAI.BorsukNine.FiniteObstruction.c10208 line 361
  41. theorem OAI.BorsukNine.FiniteObstruction.c10213 line 369
  42. theorem OAI.BorsukNine.FiniteObstruction.c10219 line 377
  43. theorem OAI.BorsukNine.FiniteObstruction.c10295 line 385
  44. theorem OAI.BorsukNine.FiniteObstruction.c10330 line 395
  45. theorem OAI.BorsukNine.FiniteObstruction.c10343 line 405
  46. theorem OAI.BorsukNine.FiniteObstruction.c10344 line 413
  47. theorem OAI.BorsukNine.FiniteObstruction.c10347 line 421
  48. theorem OAI.BorsukNine.FiniteObstruction.c10359 line 429