OAI/Geometry/Borsuk/FiniteCases/Cases034.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c8513 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c8520 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c8527 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c8528 line 39
  5. theorem OAI.BorsukNine.FiniteObstruction.c8531 line 47
  6. theorem OAI.BorsukNine.FiniteObstruction.c8568 line 55
  7. theorem OAI.BorsukNine.FiniteObstruction.c8615 line 65
  8. theorem OAI.BorsukNine.FiniteObstruction.c8625 line 75
  9. theorem OAI.BorsukNine.FiniteObstruction.c8626 line 85
  10. theorem OAI.BorsukNine.FiniteObstruction.c8627 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c8633 line 105
  12. theorem OAI.BorsukNine.FiniteObstruction.c8648 line 115
  13. theorem OAI.BorsukNine.FiniteObstruction.c8652 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c8662 line 135
  15. theorem OAI.BorsukNine.FiniteObstruction.c8664 line 143
  16. theorem OAI.BorsukNine.FiniteObstruction.c8666 line 151
  17. theorem OAI.BorsukNine.FiniteObstruction.c8789 line 159
  18. theorem OAI.BorsukNine.FiniteObstruction.c8799 line 169
  19. theorem OAI.BorsukNine.FiniteObstruction.c8804 line 179
  20. theorem OAI.BorsukNine.FiniteObstruction.c8805 line 187
  21. theorem OAI.BorsukNine.FiniteObstruction.c8813 line 195
  22. theorem OAI.BorsukNine.FiniteObstruction.c8857 line 203
  23. theorem OAI.BorsukNine.FiniteObstruction.c8889 line 213
  24. theorem OAI.BorsukNine.FiniteObstruction.c8903 line 223
  25. theorem OAI.BorsukNine.FiniteObstruction.c8905 line 233
  26. theorem OAI.BorsukNine.FiniteObstruction.c8915 line 243
  27. theorem OAI.BorsukNine.FiniteObstruction.c8939 line 253
  28. theorem OAI.BorsukNine.FiniteObstruction.c8940 line 263
  29. theorem OAI.BorsukNine.FiniteObstruction.c8942 line 273
  30. theorem OAI.BorsukNine.FiniteObstruction.c8944 line 281
  31. theorem OAI.BorsukNine.FiniteObstruction.c8945 line 289
  32. theorem OAI.BorsukNine.FiniteObstruction.c8948 line 297
  33. theorem OAI.BorsukNine.FiniteObstruction.c8952 line 305
  34. theorem OAI.BorsukNine.FiniteObstruction.c8953 line 313
  35. theorem OAI.BorsukNine.FiniteObstruction.c9037 line 321
  36. theorem OAI.BorsukNine.FiniteObstruction.c9045 line 331
  37. theorem OAI.BorsukNine.FiniteObstruction.c9047 line 341
  38. theorem OAI.BorsukNine.FiniteObstruction.c9071 line 351
  39. theorem OAI.BorsukNine.FiniteObstruction.c9073 line 361
  40. theorem OAI.BorsukNine.FiniteObstruction.c9079 line 371
  41. theorem OAI.BorsukNine.FiniteObstruction.c9082 line 381
  42. theorem OAI.BorsukNine.FiniteObstruction.c9084 line 389
  43. theorem OAI.BorsukNine.FiniteObstruction.c9086 line 397
  44. theorem OAI.BorsukNine.FiniteObstruction.c9087 line 405
  45. theorem OAI.BorsukNine.FiniteObstruction.c9115 line 413
  46. theorem OAI.BorsukNine.FiniteObstruction.c9151 line 423