OAI/Geometry/Borsuk/FiniteCases/Cases076.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c29971 line 12
  2. theorem OAI.BorsukNine.FiniteObstruction.c29979 line 22
  3. theorem OAI.BorsukNine.FiniteObstruction.c29986 line 32
  4. theorem OAI.BorsukNine.FiniteObstruction.c30103 line 42
  5. theorem OAI.BorsukNine.FiniteObstruction.c30111 line 52
  6. theorem OAI.BorsukNine.FiniteObstruction.c30119 line 62
  7. theorem OAI.BorsukNine.FiniteObstruction.c30126 line 72
  8. theorem OAI.BorsukNine.FiniteObstruction.c30243 line 82
  9. theorem OAI.BorsukNine.FiniteObstruction.c30251 line 92
  10. theorem OAI.BorsukNine.FiniteObstruction.c30259 line 102
  11. theorem OAI.BorsukNine.FiniteObstruction.c30266 line 112
  12. theorem OAI.BorsukNine.FiniteObstruction.c30383 line 122
  13. theorem OAI.BorsukNine.FiniteObstruction.c30391 line 132
  14. theorem OAI.BorsukNine.FiniteObstruction.c30399 line 142
  15. theorem OAI.BorsukNine.FiniteObstruction.c30406 line 152
  16. theorem OAI.BorsukNine.FiniteObstruction.c30523 line 162
  17. theorem OAI.BorsukNine.FiniteObstruction.c30531 line 172
  18. theorem OAI.BorsukNine.FiniteObstruction.c30539 line 182
  19. theorem OAI.BorsukNine.FiniteObstruction.c30546 line 192
  20. theorem OAI.BorsukNine.FiniteObstruction.c30663 line 202
  21. theorem OAI.BorsukNine.FiniteObstruction.c30671 line 212
  22. theorem OAI.BorsukNine.FiniteObstruction.c30679 line 222
  23. theorem OAI.BorsukNine.FiniteObstruction.c30686 line 232
  24. theorem OAI.BorsukNine.FiniteObstruction.c30803 line 242
  25. theorem OAI.BorsukNine.FiniteObstruction.c30811 line 252
  26. theorem OAI.BorsukNine.FiniteObstruction.c30819 line 262
  27. theorem OAI.BorsukNine.FiniteObstruction.c30826 line 272
  28. theorem OAI.BorsukNine.FiniteObstruction.c30943 line 282
  29. theorem OAI.BorsukNine.FiniteObstruction.c30951 line 292
  30. theorem OAI.BorsukNine.FiniteObstruction.c30959 line 302
  31. theorem OAI.BorsukNine.FiniteObstruction.c30966 line 312
  32. theorem OAI.BorsukNine.FiniteObstruction.c31083 line 322
  33. theorem OAI.BorsukNine.FiniteObstruction.c31091 line 332
  34. theorem OAI.BorsukNine.FiniteObstruction.c31099 line 342
  35. theorem OAI.BorsukNine.FiniteObstruction.c31106 line 352
  36. theorem OAI.BorsukNine.FiniteObstruction.c31202 line 362
  37. theorem OAI.BorsukNine.FiniteObstruction.c31203 line 366
  38. theorem OAI.BorsukNine.FiniteObstruction.c31204 line 375
  39. theorem OAI.BorsukNine.FiniteObstruction.c31205 line 384
  40. theorem OAI.BorsukNine.FiniteObstruction.c31206 line 393
  41. theorem OAI.BorsukNine.FiniteObstruction.c31207 line 402
  42. theorem OAI.BorsukNine.FiniteObstruction.c31208 line 426