OAI/Geometry/Borsuk/FiniteCases/Cases031.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c6849 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c6850 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c6852 line 27
  4. theorem OAI.BorsukNine.FiniteObstruction.c6865 line 35
  5. theorem OAI.BorsukNine.FiniteObstruction.c6897 line 45
  6. theorem OAI.BorsukNine.FiniteObstruction.c6902 line 55
  7. theorem OAI.BorsukNine.FiniteObstruction.c6909 line 65
  8. theorem OAI.BorsukNine.FiniteObstruction.c6929 line 75
  9. theorem OAI.BorsukNine.FiniteObstruction.c6935 line 85
  10. theorem OAI.BorsukNine.FiniteObstruction.c6942 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c6947 line 105
  12. theorem OAI.BorsukNine.FiniteObstruction.c6974 line 115
  13. theorem OAI.BorsukNine.FiniteObstruction.c6975 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c6976 line 135
  15. theorem OAI.BorsukNine.FiniteObstruction.c6980 line 145
  16. theorem OAI.BorsukNine.FiniteObstruction.c6985 line 155
  17. theorem OAI.BorsukNine.FiniteObstruction.c6988 line 163
  18. theorem OAI.BorsukNine.FiniteObstruction.c6989 line 171
  19. theorem OAI.BorsukNine.FiniteObstruction.c7009 line 179
  20. theorem OAI.BorsukNine.FiniteObstruction.c7075 line 189
  21. theorem OAI.BorsukNine.FiniteObstruction.c7081 line 199
  22. theorem OAI.BorsukNine.FiniteObstruction.c7082 line 209
  23. theorem OAI.BorsukNine.FiniteObstruction.c7089 line 219
  24. theorem OAI.BorsukNine.FiniteObstruction.c7091 line 229
  25. theorem OAI.BorsukNine.FiniteObstruction.c7093 line 239
  26. theorem OAI.BorsukNine.FiniteObstruction.c7098 line 249
  27. theorem OAI.BorsukNine.FiniteObstruction.c7101 line 259
  28. theorem OAI.BorsukNine.FiniteObstruction.c7109 line 269
  29. theorem OAI.BorsukNine.FiniteObstruction.c7122 line 279
  30. theorem OAI.BorsukNine.FiniteObstruction.c7123 line 287
  31. theorem OAI.BorsukNine.FiniteObstruction.c7125 line 295
  32. theorem OAI.BorsukNine.FiniteObstruction.c7126 line 303
  33. theorem OAI.BorsukNine.FiniteObstruction.c7131 line 311
  34. theorem OAI.BorsukNine.FiniteObstruction.c7132 line 319
  35. theorem OAI.BorsukNine.FiniteObstruction.c7151 line 327
  36. theorem OAI.BorsukNine.FiniteObstruction.c7155 line 337
  37. theorem OAI.BorsukNine.FiniteObstruction.c7197 line 347
  38. theorem OAI.BorsukNine.FiniteObstruction.c7215 line 357
  39. theorem OAI.BorsukNine.FiniteObstruction.c7231 line 367
  40. theorem OAI.BorsukNine.FiniteObstruction.c7234 line 377
  41. theorem OAI.BorsukNine.FiniteObstruction.c7237 line 387
  42. theorem OAI.BorsukNine.FiniteObstruction.c7238 line 397
  43. theorem OAI.BorsukNine.FiniteObstruction.c7241 line 407
  44. theorem OAI.BorsukNine.FiniteObstruction.c7242 line 417
  45. theorem OAI.BorsukNine.FiniteObstruction.c7248 line 427