OAI/Geometry/Borsuk/FiniteCases/Cases061.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c22528 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c22542 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c22565 line 29
  4. theorem OAI.BorsukNine.FiniteObstruction.c22597 line 39
  5. theorem OAI.BorsukNine.FiniteObstruction.c22615 line 49
  6. theorem OAI.BorsukNine.FiniteObstruction.c22618 line 59
  7. theorem OAI.BorsukNine.FiniteObstruction.c22621 line 69
  8. theorem OAI.BorsukNine.FiniteObstruction.c22627 line 79
  9. theorem OAI.BorsukNine.FiniteObstruction.c22640 line 89
  10. theorem OAI.BorsukNine.FiniteObstruction.c22642 line 99
  11. theorem OAI.BorsukNine.FiniteObstruction.c22651 line 109
  12. theorem OAI.BorsukNine.FiniteObstruction.c22663 line 119
  13. theorem OAI.BorsukNine.FiniteObstruction.c22664 line 127
  14. theorem OAI.BorsukNine.FiniteObstruction.c22665 line 135
  15. theorem OAI.BorsukNine.FiniteObstruction.c22668 line 143
  16. theorem OAI.BorsukNine.FiniteObstruction.c22670 line 151
  17. theorem OAI.BorsukNine.FiniteObstruction.c22674 line 159
  18. theorem OAI.BorsukNine.FiniteObstruction.c22677 line 167
  19. theorem OAI.BorsukNine.FiniteObstruction.c22679 line 175
  20. theorem OAI.BorsukNine.FiniteObstruction.c22681 line 183
  21. theorem OAI.BorsukNine.FiniteObstruction.c22690 line 191
  22. theorem OAI.BorsukNine.FiniteObstruction.c22723 line 201
  23. theorem OAI.BorsukNine.FiniteObstruction.c22724 line 211
  24. theorem OAI.BorsukNine.FiniteObstruction.c22725 line 221
  25. theorem OAI.BorsukNine.FiniteObstruction.c22726 line 231
  26. theorem OAI.BorsukNine.FiniteObstruction.c22766 line 241
  27. theorem OAI.BorsukNine.FiniteObstruction.c22777 line 251
  28. theorem OAI.BorsukNine.FiniteObstruction.c22780 line 261
  29. theorem OAI.BorsukNine.FiniteObstruction.c22781 line 271
  30. theorem OAI.BorsukNine.FiniteObstruction.c22783 line 281
  31. theorem OAI.BorsukNine.FiniteObstruction.c22784 line 291
  32. theorem OAI.BorsukNine.FiniteObstruction.c22799 line 301
  33. theorem OAI.BorsukNine.FiniteObstruction.c22801 line 311
  34. theorem OAI.BorsukNine.FiniteObstruction.c22802 line 321
  35. theorem OAI.BorsukNine.FiniteObstruction.c22804 line 329
  36. theorem OAI.BorsukNine.FiniteObstruction.c22805 line 337
  37. theorem OAI.BorsukNine.FiniteObstruction.c22811 line 345
  38. theorem OAI.BorsukNine.FiniteObstruction.c22813 line 353
  39. theorem OAI.BorsukNine.FiniteObstruction.c22831 line 361
  40. theorem OAI.BorsukNine.FiniteObstruction.c22838 line 371
  41. theorem OAI.BorsukNine.FiniteObstruction.c22840 line 381
  42. theorem OAI.BorsukNine.FiniteObstruction.c22847 line 391
  43. theorem OAI.BorsukNine.FiniteObstruction.c22861 line 401
  44. theorem OAI.BorsukNine.FiniteObstruction.c22863 line 411
  45. theorem OAI.BorsukNine.FiniteObstruction.c22871 line 421