OAI/Geometry/Borsuk/FiniteCases/Cases054.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c18851 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c18862 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c18875 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c18889 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c18894 line 49
  6. theorem OAI.BorsukNine.FiniteObstruction.c18896 line 57
  7. theorem OAI.BorsukNine.FiniteObstruction.c18903 line 65
  8. theorem OAI.BorsukNine.FiniteObstruction.c18913 line 75
  9. theorem OAI.BorsukNine.FiniteObstruction.c18915 line 85
  10. theorem OAI.BorsukNine.FiniteObstruction.c18937 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c18943 line 105
  12. theorem OAI.BorsukNine.FiniteObstruction.c18954 line 115
  13. theorem OAI.BorsukNine.FiniteObstruction.c18958 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c18962 line 135
  15. theorem OAI.BorsukNine.FiniteObstruction.c18966 line 145
  16. theorem OAI.BorsukNine.FiniteObstruction.c18969 line 155
  17. theorem OAI.BorsukNine.FiniteObstruction.c18991 line 165
  18. theorem OAI.BorsukNine.FiniteObstruction.c18995 line 175
  19. theorem OAI.BorsukNine.FiniteObstruction.c18997 line 185
  20. theorem OAI.BorsukNine.FiniteObstruction.c19000 line 195
  21. theorem OAI.BorsukNine.FiniteObstruction.c19002 line 205
  22. theorem OAI.BorsukNine.FiniteObstruction.c19004 line 215
  23. theorem OAI.BorsukNine.FiniteObstruction.c19018 line 225
  24. theorem OAI.BorsukNine.FiniteObstruction.c19023 line 235
  25. theorem OAI.BorsukNine.FiniteObstruction.c19043 line 243
  26. theorem OAI.BorsukNine.FiniteObstruction.c19055 line 253
  27. theorem OAI.BorsukNine.FiniteObstruction.c19091 line 263
  28. theorem OAI.BorsukNine.FiniteObstruction.c19099 line 273
  29. theorem OAI.BorsukNine.FiniteObstruction.c19139 line 283
  30. theorem OAI.BorsukNine.FiniteObstruction.c19163 line 293
  31. theorem OAI.BorsukNine.FiniteObstruction.c19165 line 301
  32. theorem OAI.BorsukNine.FiniteObstruction.c19167 line 309
  33. theorem OAI.BorsukNine.FiniteObstruction.c19169 line 317
  34. theorem OAI.BorsukNine.FiniteObstruction.c19175 line 325
  35. theorem OAI.BorsukNine.FiniteObstruction.c19176 line 333
  36. theorem OAI.BorsukNine.FiniteObstruction.c19177 line 341
  37. theorem OAI.BorsukNine.FiniteObstruction.c19183 line 349
  38. theorem OAI.BorsukNine.FiniteObstruction.c19191 line 359
  39. theorem OAI.BorsukNine.FiniteObstruction.c19225 line 369
  40. theorem OAI.BorsukNine.FiniteObstruction.c19227 line 379
  41. theorem OAI.BorsukNine.FiniteObstruction.c19246 line 389
  42. theorem OAI.BorsukNine.FiniteObstruction.c19248 line 399
  43. theorem OAI.BorsukNine.FiniteObstruction.c19272 line 409
  44. theorem OAI.BorsukNine.FiniteObstruction.c19279 line 419
  45. theorem OAI.BorsukNine.FiniteObstruction.c19280 line 429