OAI/Geometry/Borsuk/FiniteCases/Cases008.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c654 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c655 line 16
  3. theorem OAI.BorsukNine.FiniteObstruction.c656 line 33
  4. theorem OAI.BorsukNine.FiniteObstruction.c660 line 38
  5. theorem OAI.BorsukNine.FiniteObstruction.c661 line 43
  6. theorem OAI.BorsukNine.FiniteObstruction.c662 line 60
  7. theorem OAI.BorsukNine.FiniteObstruction.c664 line 77
  8. theorem OAI.BorsukNine.FiniteObstruction.c665 line 94
  9. theorem OAI.BorsukNine.FiniteObstruction.c669 line 99
  10. theorem OAI.BorsukNine.FiniteObstruction.c671 line 104
  11. theorem OAI.BorsukNine.FiniteObstruction.c673 line 109
  12. theorem OAI.BorsukNine.FiniteObstruction.c674 line 114
  13. theorem OAI.BorsukNine.FiniteObstruction.c675 line 131
  14. theorem OAI.BorsukNine.FiniteObstruction.c677 line 136
  15. theorem OAI.BorsukNine.FiniteObstruction.c678 line 153
  16. theorem OAI.BorsukNine.FiniteObstruction.c679 line 158
  17. theorem OAI.BorsukNine.FiniteObstruction.c680 line 175
  18. theorem OAI.BorsukNine.FiniteObstruction.c682 line 180
  19. theorem OAI.BorsukNine.FiniteObstruction.c684 line 185
  20. theorem OAI.BorsukNine.FiniteObstruction.c686 line 190
  21. theorem OAI.BorsukNine.FiniteObstruction.c687 line 195
  22. theorem OAI.BorsukNine.FiniteObstruction.c688 line 212
  23. theorem OAI.BorsukNine.FiniteObstruction.c690 line 217
  24. theorem OAI.BorsukNine.FiniteObstruction.c692 line 222
  25. theorem OAI.BorsukNine.FiniteObstruction.c694 line 239
  26. theorem OAI.BorsukNine.FiniteObstruction.c695 line 256
  27. theorem OAI.BorsukNine.FiniteObstruction.c696 line 261
  28. theorem OAI.BorsukNine.FiniteObstruction.c701 line 278
  29. theorem OAI.BorsukNine.FiniteObstruction.c705 line 283
  30. theorem OAI.BorsukNine.FiniteObstruction.c714 line 288
  31. theorem OAI.BorsukNine.FiniteObstruction.c715 line 293
  32. theorem OAI.BorsukNine.FiniteObstruction.c716 line 310
  33. theorem OAI.BorsukNine.FiniteObstruction.c720 line 315
  34. theorem OAI.BorsukNine.FiniteObstruction.c722 line 320
  35. theorem OAI.BorsukNine.FiniteObstruction.c723 line 337
  36. theorem OAI.BorsukNine.FiniteObstruction.c724 line 342
  37. theorem OAI.BorsukNine.FiniteObstruction.c725 line 359
  38. theorem OAI.BorsukNine.FiniteObstruction.c727 line 364
  39. theorem OAI.BorsukNine.FiniteObstruction.c728 line 369
  40. theorem OAI.BorsukNine.FiniteObstruction.c729 line 386
  41. theorem OAI.BorsukNine.FiniteObstruction.c730 line 391
  42. theorem OAI.BorsukNine.FiniteObstruction.c731 line 408
  43. theorem OAI.BorsukNine.FiniteObstruction.c732 line 413