OAI/Geometry/Borsuk/FiniteCases/Cases068.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c26723 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c26731 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c26736 line 27
  4. theorem OAI.BorsukNine.FiniteObstruction.c26743 line 35
  5. theorem OAI.BorsukNine.FiniteObstruction.c26751 line 45
  6. theorem OAI.BorsukNine.FiniteObstruction.c26755 line 55
  7. theorem OAI.BorsukNine.FiniteObstruction.c26783 line 65
  8. theorem OAI.BorsukNine.FiniteObstruction.c26785 line 75
  9. theorem OAI.BorsukNine.FiniteObstruction.c26787 line 85
  10. theorem OAI.BorsukNine.FiniteObstruction.c26839 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c26863 line 105
  12. theorem OAI.BorsukNine.FiniteObstruction.c26869 line 113
  13. theorem OAI.BorsukNine.FiniteObstruction.c26870 line 121
  14. theorem OAI.BorsukNine.FiniteObstruction.c26871 line 129
  15. theorem OAI.BorsukNine.FiniteObstruction.c26875 line 137
  16. theorem OAI.BorsukNine.FiniteObstruction.c26876 line 145
  17. theorem OAI.BorsukNine.FiniteObstruction.c26877 line 153
  18. theorem OAI.BorsukNine.FiniteObstruction.c26891 line 161
  19. theorem OAI.BorsukNine.FiniteObstruction.c26893 line 171
  20. theorem OAI.BorsukNine.FiniteObstruction.c26896 line 181
  21. theorem OAI.BorsukNine.FiniteObstruction.c26899 line 191
  22. theorem OAI.BorsukNine.FiniteObstruction.c26905 line 201
  23. theorem OAI.BorsukNine.FiniteObstruction.c26913 line 211
  24. theorem OAI.BorsukNine.FiniteObstruction.c26914 line 221
  25. theorem OAI.BorsukNine.FiniteObstruction.c26916 line 231
  26. theorem OAI.BorsukNine.FiniteObstruction.c26925 line 241
  27. theorem OAI.BorsukNine.FiniteObstruction.c26927 line 251
  28. theorem OAI.BorsukNine.FiniteObstruction.c26948 line 261
  29. theorem OAI.BorsukNine.FiniteObstruction.c26952 line 271
  30. theorem OAI.BorsukNine.FiniteObstruction.c26979 line 281
  31. theorem OAI.BorsukNine.FiniteObstruction.c26980 line 291
  32. theorem OAI.BorsukNine.FiniteObstruction.c26982 line 301
  33. theorem OAI.BorsukNine.FiniteObstruction.c26984 line 311
  34. theorem OAI.BorsukNine.FiniteObstruction.c26996 line 321
  35. theorem OAI.BorsukNine.FiniteObstruction.c27000 line 331
  36. theorem OAI.BorsukNine.FiniteObstruction.c27012 line 341
  37. theorem OAI.BorsukNine.FiniteObstruction.c27013 line 349
  38. theorem OAI.BorsukNine.FiniteObstruction.c27017 line 357
  39. theorem OAI.BorsukNine.FiniteObstruction.c27020 line 365
  40. theorem OAI.BorsukNine.FiniteObstruction.c27025 line 373
  41. theorem OAI.BorsukNine.FiniteObstruction.c27031 line 383
  42. theorem OAI.BorsukNine.FiniteObstruction.c27063 line 393
  43. theorem OAI.BorsukNine.FiniteObstruction.c27065 line 403
  44. theorem OAI.BorsukNine.FiniteObstruction.c27067 line 413
  45. theorem OAI.BorsukNine.FiniteObstruction.c27102 line 423