OAI/Geometry/Borsuk/FiniteCases/Cases058.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c20828 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c20830 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c20838 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c20840 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c20850 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c20856 line 59
  7. theorem OAI.BorsukNine.FiniteObstruction.c20858 line 67
  8. theorem OAI.BorsukNine.FiniteObstruction.c20868 line 75
  9. theorem OAI.BorsukNine.FiniteObstruction.c20878 line 85
  10. theorem OAI.BorsukNine.FiniteObstruction.c20895 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c20957 line 105
  12. theorem OAI.BorsukNine.FiniteObstruction.c20967 line 115
  13. theorem OAI.BorsukNine.FiniteObstruction.c20983 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c20990 line 133
  15. theorem OAI.BorsukNine.FiniteObstruction.c20995 line 141
  16. theorem OAI.BorsukNine.FiniteObstruction.c21000 line 149
  17. theorem OAI.BorsukNine.FiniteObstruction.c21001 line 157
  18. theorem OAI.BorsukNine.FiniteObstruction.c21018 line 165
  19. theorem OAI.BorsukNine.FiniteObstruction.c21022 line 175
  20. theorem OAI.BorsukNine.FiniteObstruction.c21039 line 185
  21. theorem OAI.BorsukNine.FiniteObstruction.c21100 line 195
  22. theorem OAI.BorsukNine.FiniteObstruction.c21104 line 205
  23. theorem OAI.BorsukNine.FiniteObstruction.c21115 line 215
  24. theorem OAI.BorsukNine.FiniteObstruction.c21118 line 225
  25. theorem OAI.BorsukNine.FiniteObstruction.c21120 line 235
  26. theorem OAI.BorsukNine.FiniteObstruction.c21123 line 245
  27. theorem OAI.BorsukNine.FiniteObstruction.c21124 line 253
  28. theorem OAI.BorsukNine.FiniteObstruction.c21126 line 261
  29. theorem OAI.BorsukNine.FiniteObstruction.c21128 line 269
  30. theorem OAI.BorsukNine.FiniteObstruction.c21132 line 277
  31. theorem OAI.BorsukNine.FiniteObstruction.c21133 line 285
  32. theorem OAI.BorsukNine.FiniteObstruction.c21139 line 293
  33. theorem OAI.BorsukNine.FiniteObstruction.c21143 line 301
  34. theorem OAI.BorsukNine.FiniteObstruction.c21145 line 311
  35. theorem OAI.BorsukNine.FiniteObstruction.c21158 line 321
  36. theorem OAI.BorsukNine.FiniteObstruction.c21192 line 331
  37. theorem OAI.BorsukNine.FiniteObstruction.c21195 line 341
  38. theorem OAI.BorsukNine.FiniteObstruction.c21214 line 351
  39. theorem OAI.BorsukNine.FiniteObstruction.c21216 line 361
  40. theorem OAI.BorsukNine.FiniteObstruction.c21222 line 371
  41. theorem OAI.BorsukNine.FiniteObstruction.c21224 line 381
  42. theorem OAI.BorsukNine.FiniteObstruction.c21247 line 391
  43. theorem OAI.BorsukNine.FiniteObstruction.c21263 line 401
  44. theorem OAI.BorsukNine.FiniteObstruction.c21269 line 409
  45. theorem OAI.BorsukNine.FiniteObstruction.c21306 line 417
  46. theorem OAI.BorsukNine.FiniteObstruction.c21308 line 427