OAI/Geometry/Borsuk/FiniteCases/Cases032.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c7251 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c7266 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c7268 line 29
  4. theorem OAI.BorsukNine.FiniteObstruction.c7269 line 37
  5. theorem OAI.BorsukNine.FiniteObstruction.c7371 line 45
  6. theorem OAI.BorsukNine.FiniteObstruction.c7395 line 55
  7. theorem OAI.BorsukNine.FiniteObstruction.c7411 line 65
  8. theorem OAI.BorsukNine.FiniteObstruction.c7425 line 73
  9. theorem OAI.BorsukNine.FiniteObstruction.c7441 line 83
  10. theorem OAI.BorsukNine.FiniteObstruction.c7469 line 93
  11. theorem OAI.BorsukNine.FiniteObstruction.c7513 line 103
  12. theorem OAI.BorsukNine.FiniteObstruction.c7534 line 113
  13. theorem OAI.BorsukNine.FiniteObstruction.c7536 line 123
  14. theorem OAI.BorsukNine.FiniteObstruction.c7548 line 133
  15. theorem OAI.BorsukNine.FiniteObstruction.c7549 line 141
  16. theorem OAI.BorsukNine.FiniteObstruction.c7555 line 149
  17. theorem OAI.BorsukNine.FiniteObstruction.c7557 line 157
  18. theorem OAI.BorsukNine.FiniteObstruction.c7565 line 165
  19. theorem OAI.BorsukNine.FiniteObstruction.c7573 line 175
  20. theorem OAI.BorsukNine.FiniteObstruction.c7578 line 185
  21. theorem OAI.BorsukNine.FiniteObstruction.c7592 line 195
  22. theorem OAI.BorsukNine.FiniteObstruction.c7597 line 205
  23. theorem OAI.BorsukNine.FiniteObstruction.c7615 line 215
  24. theorem OAI.BorsukNine.FiniteObstruction.c7621 line 225
  25. theorem OAI.BorsukNine.FiniteObstruction.c7625 line 235
  26. theorem OAI.BorsukNine.FiniteObstruction.c7634 line 245
  27. theorem OAI.BorsukNine.FiniteObstruction.c7635 line 255
  28. theorem OAI.BorsukNine.FiniteObstruction.c7639 line 265
  29. theorem OAI.BorsukNine.FiniteObstruction.c7640 line 275
  30. theorem OAI.BorsukNine.FiniteObstruction.c7647 line 285
  31. theorem OAI.BorsukNine.FiniteObstruction.c7649 line 295
  32. theorem OAI.BorsukNine.FiniteObstruction.c7683 line 305
  33. theorem OAI.BorsukNine.FiniteObstruction.c7685 line 313
  34. theorem OAI.BorsukNine.FiniteObstruction.c7688 line 321
  35. theorem OAI.BorsukNine.FiniteObstruction.c7689 line 329
  36. theorem OAI.BorsukNine.FiniteObstruction.c7695 line 337
  37. theorem OAI.BorsukNine.FiniteObstruction.c7718 line 345
  38. theorem OAI.BorsukNine.FiniteObstruction.c7774 line 355
  39. theorem OAI.BorsukNine.FiniteObstruction.c7775 line 365
  40. theorem OAI.BorsukNine.FiniteObstruction.c7783 line 375
  41. theorem OAI.BorsukNine.FiniteObstruction.c7805 line 385
  42. theorem OAI.BorsukNine.FiniteObstruction.c7823 line 395
  43. theorem OAI.BorsukNine.FiniteObstruction.c7828 line 403
  44. theorem OAI.BorsukNine.FiniteObstruction.c7829 line 411
  45. theorem OAI.BorsukNine.FiniteObstruction.c7837 line 419
  46. theorem OAI.BorsukNine.FiniteObstruction.c7841 line 427