OAI/Geometry/Borsuk/FiniteCases/Cases105.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c31667 line 14
  2. theorem OAI.BorsukNine.FiniteObstruction.c31668 line 23
  3. theorem OAI.BorsukNine.FiniteObstruction.c31669 line 32
  4. theorem OAI.BorsukNine.FiniteObstruction.c31670 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c31671 line 50
  6. theorem OAI.BorsukNine.FiniteObstruction.c31672 line 59
  7. theorem OAI.BorsukNine.FiniteObstruction.c31673 line 68
  8. theorem OAI.BorsukNine.FiniteObstruction.c31675 line 77
  9. theorem OAI.BorsukNine.FiniteObstruction.c31677 line 86
  10. theorem OAI.BorsukNine.FiniteObstruction.c31678 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c31680 line 104
  12. theorem OAI.BorsukNine.FiniteObstruction.c31681 line 113
  13. theorem OAI.BorsukNine.FiniteObstruction.c31683 line 122
  14. theorem OAI.BorsukNine.FiniteObstruction.c31685 line 131
  15. theorem OAI.BorsukNine.FiniteObstruction.c31690 line 140
  16. theorem OAI.BorsukNine.FiniteObstruction.c31691 line 149
  17. theorem OAI.BorsukNine.FiniteObstruction.c31692 line 158
  18. theorem OAI.BorsukNine.FiniteObstruction.c31693 line 167
  19. theorem OAI.BorsukNine.FiniteObstruction.c31703 line 176
  20. theorem OAI.BorsukNine.FiniteObstruction.c31704 line 185
  21. theorem OAI.BorsukNine.FiniteObstruction.c31705 line 194
  22. theorem OAI.BorsukNine.FiniteObstruction.c31706 line 203
  23. theorem OAI.BorsukNine.FiniteObstruction.c31707 line 212
  24. theorem OAI.BorsukNine.FiniteObstruction.c31708 line 221
  25. theorem OAI.BorsukNine.FiniteObstruction.c31709 line 230
  26. theorem OAI.BorsukNine.FiniteObstruction.c31710 line 239
  27. theorem OAI.BorsukNine.FiniteObstruction.c31711 line 248
  28. theorem OAI.BorsukNine.FiniteObstruction.c31712 line 257
  29. theorem OAI.BorsukNine.FiniteObstruction.c31714 line 266
  30. theorem OAI.BorsukNine.FiniteObstruction.c31715 line 275
  31. theorem OAI.BorsukNine.FiniteObstruction.c31718 line 284
  32. theorem OAI.BorsukNine.FiniteObstruction.c31720 line 293
  33. theorem OAI.BorsukNine.FiniteObstruction.c31721 line 302
  34. theorem OAI.BorsukNine.FiniteObstruction.c31722 line 311
  35. theorem OAI.BorsukNine.FiniteObstruction.c31723 line 320
  36. theorem OAI.BorsukNine.FiniteObstruction.c31724 line 329
  37. theorem OAI.BorsukNine.FiniteObstruction.c31725 line 338
  38. theorem OAI.BorsukNine.FiniteObstruction.c31726 line 347
  39. theorem OAI.BorsukNine.FiniteObstruction.c31727 line 356
  40. theorem OAI.BorsukNine.FiniteObstruction.c31731 line 365
  41. theorem OAI.BorsukNine.FiniteObstruction.c31732 line 374
  42. theorem OAI.BorsukNine.FiniteObstruction.c31733 line 383
  43. theorem OAI.BorsukNine.FiniteObstruction.c31735 line 392
  44. theorem OAI.BorsukNine.FiniteObstruction.c31737 line 401
  45. theorem OAI.BorsukNine.FiniteObstruction.c31738 line 410
  46. theorem OAI.BorsukNine.FiniteObstruction.c31739 line 419
  47. theorem OAI.BorsukNine.FiniteObstruction.c31741 line 428