OAI/Geometry/Borsuk/FiniteCases/Cases071.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c27873 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c27875 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c27878 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c27901 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c27905 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c27907 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c27928 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c27931 line 81
  9. theorem OAI.BorsukNine.FiniteObstruction.c27947 line 91
  10. theorem OAI.BorsukNine.FiniteObstruction.c27950 line 101
  11. theorem OAI.BorsukNine.FiniteObstruction.c27952 line 111
  12. theorem OAI.BorsukNine.FiniteObstruction.c27955 line 121
  13. theorem OAI.BorsukNine.FiniteObstruction.c27959 line 131
  14. theorem OAI.BorsukNine.FiniteObstruction.c27960 line 141
  15. theorem OAI.BorsukNine.FiniteObstruction.c27964 line 151
  16. theorem OAI.BorsukNine.FiniteObstruction.c27967 line 161
  17. theorem OAI.BorsukNine.FiniteObstruction.c27970 line 171
  18. theorem OAI.BorsukNine.FiniteObstruction.c27983 line 181
  19. theorem OAI.BorsukNine.FiniteObstruction.c28015 line 189
  20. theorem OAI.BorsukNine.FiniteObstruction.c28047 line 199
  21. theorem OAI.BorsukNine.FiniteObstruction.c28083 line 209
  22. theorem OAI.BorsukNine.FiniteObstruction.c28099 line 219
  23. theorem OAI.BorsukNine.FiniteObstruction.c28123 line 229
  24. theorem OAI.BorsukNine.FiniteObstruction.c28124 line 237
  25. theorem OAI.BorsukNine.FiniteObstruction.c28128 line 245
  26. theorem OAI.BorsukNine.FiniteObstruction.c28129 line 253
  27. theorem OAI.BorsukNine.FiniteObstruction.c28130 line 261
  28. theorem OAI.BorsukNine.FiniteObstruction.c28131 line 269
  29. theorem OAI.BorsukNine.FiniteObstruction.c28134 line 277
  30. theorem OAI.BorsukNine.FiniteObstruction.c28135 line 285
  31. theorem OAI.BorsukNine.FiniteObstruction.c28136 line 293
  32. theorem OAI.BorsukNine.FiniteObstruction.c28137 line 301
  33. theorem OAI.BorsukNine.FiniteObstruction.c28140 line 309
  34. theorem OAI.BorsukNine.FiniteObstruction.c28143 line 317
  35. theorem OAI.BorsukNine.FiniteObstruction.c28153 line 327
  36. theorem OAI.BorsukNine.FiniteObstruction.c28156 line 337
  37. theorem OAI.BorsukNine.FiniteObstruction.c28179 line 347
  38. theorem OAI.BorsukNine.FiniteObstruction.c28181 line 357
  39. theorem OAI.BorsukNine.FiniteObstruction.c28183 line 367
  40. theorem OAI.BorsukNine.FiniteObstruction.c28185 line 377
  41. theorem OAI.BorsukNine.FiniteObstruction.c28187 line 387
  42. theorem OAI.BorsukNine.FiniteObstruction.c28191 line 397
  43. theorem OAI.BorsukNine.FiniteObstruction.c28195 line 407
  44. theorem OAI.BorsukNine.FiniteObstruction.c28197 line 417
  45. theorem OAI.BorsukNine.FiniteObstruction.c28208 line 427