OAI/Geometry/Borsuk/FiniteCases/Cases056.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c19943 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c19949 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c19951 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c19980 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c19982 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c19995 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c20003 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c20004 line 79
  9. theorem OAI.BorsukNine.FiniteObstruction.c20008 line 87
  10. theorem OAI.BorsukNine.FiniteObstruction.c20010 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c20016 line 103
  12. theorem OAI.BorsukNine.FiniteObstruction.c20025 line 111
  13. theorem OAI.BorsukNine.FiniteObstruction.c20028 line 121
  14. theorem OAI.BorsukNine.FiniteObstruction.c20055 line 131
  15. theorem OAI.BorsukNine.FiniteObstruction.c20117 line 141
  16. theorem OAI.BorsukNine.FiniteObstruction.c20127 line 151
  17. theorem OAI.BorsukNine.FiniteObstruction.c20135 line 161
  18. theorem OAI.BorsukNine.FiniteObstruction.c20143 line 171
  19. theorem OAI.BorsukNine.FiniteObstruction.c20149 line 179
  20. theorem OAI.BorsukNine.FiniteObstruction.c20151 line 187
  21. theorem OAI.BorsukNine.FiniteObstruction.c20154 line 195
  22. theorem OAI.BorsukNine.FiniteObstruction.c20155 line 203
  23. theorem OAI.BorsukNine.FiniteObstruction.c20156 line 211
  24. theorem OAI.BorsukNine.FiniteObstruction.c20157 line 219
  25. theorem OAI.BorsukNine.FiniteObstruction.c20158 line 227
  26. theorem OAI.BorsukNine.FiniteObstruction.c20163 line 235
  27. theorem OAI.BorsukNine.FiniteObstruction.c20205 line 245
  28. theorem OAI.BorsukNine.FiniteObstruction.c20207 line 255
  29. theorem OAI.BorsukNine.FiniteObstruction.c20220 line 265
  30. theorem OAI.BorsukNine.FiniteObstruction.c20226 line 275
  31. theorem OAI.BorsukNine.FiniteObstruction.c20228 line 285
  32. theorem OAI.BorsukNine.FiniteObstruction.c20234 line 295
  33. theorem OAI.BorsukNine.FiniteObstruction.c20236 line 305
  34. theorem OAI.BorsukNine.FiniteObstruction.c20251 line 315
  35. theorem OAI.BorsukNine.FiniteObstruction.c20255 line 325
  36. theorem OAI.BorsukNine.FiniteObstruction.c20259 line 335
  37. theorem OAI.BorsukNine.FiniteObstruction.c20260 line 345
  38. theorem OAI.BorsukNine.FiniteObstruction.c20262 line 355
  39. theorem OAI.BorsukNine.FiniteObstruction.c20283 line 365
  40. theorem OAI.BorsukNine.FiniteObstruction.c20288 line 373
  41. theorem OAI.BorsukNine.FiniteObstruction.c20294 line 381
  42. theorem OAI.BorsukNine.FiniteObstruction.c20303 line 389
  43. theorem OAI.BorsukNine.FiniteObstruction.c20315 line 399
  44. theorem OAI.BorsukNine.FiniteObstruction.c20350 line 409
  45. theorem OAI.BorsukNine.FiniteObstruction.c20399 line 419
  46. theorem OAI.BorsukNine.FiniteObstruction.c20425 line 429