OAI/Geometry/Borsuk/FiniteCases/Cases067.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c26087 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c26103 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c26121 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c26139 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c26147 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c26168 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c26172 line 69
  8. theorem OAI.BorsukNine.FiniteObstruction.c26175 line 77
  9. theorem OAI.BorsukNine.FiniteObstruction.c26227 line 85
  10. theorem OAI.BorsukNine.FiniteObstruction.c26259 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c26287 line 105
  12. theorem OAI.BorsukNine.FiniteObstruction.c26303 line 115
  13. theorem OAI.BorsukNine.FiniteObstruction.c26310 line 123
  14. theorem OAI.BorsukNine.FiniteObstruction.c26311 line 131
  15. theorem OAI.BorsukNine.FiniteObstruction.c26312 line 139
  16. theorem OAI.BorsukNine.FiniteObstruction.c26317 line 147
  17. theorem OAI.BorsukNine.FiniteObstruction.c26318 line 155
  18. theorem OAI.BorsukNine.FiniteObstruction.c26320 line 163
  19. theorem OAI.BorsukNine.FiniteObstruction.c26331 line 171
  20. theorem OAI.BorsukNine.FiniteObstruction.c26363 line 181
  21. theorem OAI.BorsukNine.FiniteObstruction.c26365 line 191
  22. theorem OAI.BorsukNine.FiniteObstruction.c26374 line 201
  23. theorem OAI.BorsukNine.FiniteObstruction.c26391 line 211
  24. theorem OAI.BorsukNine.FiniteObstruction.c26417 line 221
  25. theorem OAI.BorsukNine.FiniteObstruction.c26450 line 231
  26. theorem OAI.BorsukNine.FiniteObstruction.c26471 line 239
  27. theorem OAI.BorsukNine.FiniteObstruction.c26473 line 249
  28. theorem OAI.BorsukNine.FiniteObstruction.c26480 line 259
  29. theorem OAI.BorsukNine.FiniteObstruction.c26497 line 269
  30. theorem OAI.BorsukNine.FiniteObstruction.c26505 line 279
  31. theorem OAI.BorsukNine.FiniteObstruction.c26583 line 289
  32. theorem OAI.BorsukNine.FiniteObstruction.c26585 line 297
  33. theorem OAI.BorsukNine.FiniteObstruction.c26587 line 305
  34. theorem OAI.BorsukNine.FiniteObstruction.c26589 line 313
  35. theorem OAI.BorsukNine.FiniteObstruction.c26597 line 321
  36. theorem OAI.BorsukNine.FiniteObstruction.c26600 line 329
  37. theorem OAI.BorsukNine.FiniteObstruction.c26605 line 337
  38. theorem OAI.BorsukNine.FiniteObstruction.c26611 line 347
  39. theorem OAI.BorsukNine.FiniteObstruction.c26643 line 357
  40. theorem OAI.BorsukNine.FiniteObstruction.c26645 line 367
  41. theorem OAI.BorsukNine.FiniteObstruction.c26647 line 377
  42. theorem OAI.BorsukNine.FiniteObstruction.c26666 line 387
  43. theorem OAI.BorsukNine.FiniteObstruction.c26671 line 397
  44. theorem OAI.BorsukNine.FiniteObstruction.c26682 line 407
  45. theorem OAI.BorsukNine.FiniteObstruction.c26704 line 417
  46. theorem OAI.BorsukNine.FiniteObstruction.c26715 line 427