OAI/Geometry/Borsuk/FiniteCases/Cases052.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c18039 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c18042 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c18043 line 29
  4. theorem OAI.BorsukNine.FiniteObstruction.c18044 line 37
  5. theorem OAI.BorsukNine.FiniteObstruction.c18045 line 45
  6. theorem OAI.BorsukNine.FiniteObstruction.c18046 line 53
  7. theorem OAI.BorsukNine.FiniteObstruction.c18047 line 61
  8. theorem OAI.BorsukNine.FiniteObstruction.c18054 line 69
  9. theorem OAI.BorsukNine.FiniteObstruction.c18055 line 77
  10. theorem OAI.BorsukNine.FiniteObstruction.c18056 line 85
  11. theorem OAI.BorsukNine.FiniteObstruction.c18057 line 93
  12. theorem OAI.BorsukNine.FiniteObstruction.c18153 line 101
  13. theorem OAI.BorsukNine.FiniteObstruction.c18158 line 111
  14. theorem OAI.BorsukNine.FiniteObstruction.c18182 line 121
  15. theorem OAI.BorsukNine.FiniteObstruction.c18184 line 129
  16. theorem OAI.BorsukNine.FiniteObstruction.c18186 line 137
  17. theorem OAI.BorsukNine.FiniteObstruction.c18237 line 145
  18. theorem OAI.BorsukNine.FiniteObstruction.c18268 line 155
  19. theorem OAI.BorsukNine.FiniteObstruction.c18275 line 165
  20. theorem OAI.BorsukNine.FiniteObstruction.c18285 line 175
  21. theorem OAI.BorsukNine.FiniteObstruction.c18322 line 185
  22. theorem OAI.BorsukNine.FiniteObstruction.c18323 line 193
  23. theorem OAI.BorsukNine.FiniteObstruction.c18324 line 201
  24. theorem OAI.BorsukNine.FiniteObstruction.c18325 line 209
  25. theorem OAI.BorsukNine.FiniteObstruction.c18326 line 217
  26. theorem OAI.BorsukNine.FiniteObstruction.c18327 line 225
  27. theorem OAI.BorsukNine.FiniteObstruction.c18328 line 233
  28. theorem OAI.BorsukNine.FiniteObstruction.c18329 line 241
  29. theorem OAI.BorsukNine.FiniteObstruction.c18336 line 249
  30. theorem OAI.BorsukNine.FiniteObstruction.c18337 line 257
  31. theorem OAI.BorsukNine.FiniteObstruction.c18339 line 265
  32. theorem OAI.BorsukNine.FiniteObstruction.c18397 line 273
  33. theorem OAI.BorsukNine.FiniteObstruction.c18405 line 283
  34. theorem OAI.BorsukNine.FiniteObstruction.c18427 line 293
  35. theorem OAI.BorsukNine.FiniteObstruction.c18430 line 303
  36. theorem OAI.BorsukNine.FiniteObstruction.c18438 line 313
  37. theorem OAI.BorsukNine.FiniteObstruction.c18440 line 323
  38. theorem OAI.BorsukNine.FiniteObstruction.c18450 line 333
  39. theorem OAI.BorsukNine.FiniteObstruction.c18452 line 343
  40. theorem OAI.BorsukNine.FiniteObstruction.c18462 line 353
  41. theorem OAI.BorsukNine.FiniteObstruction.c18463 line 361
  42. theorem OAI.BorsukNine.FiniteObstruction.c18464 line 369
  43. theorem OAI.BorsukNine.FiniteObstruction.c18465 line 377
  44. theorem OAI.BorsukNine.FiniteObstruction.c18466 line 385
  45. theorem OAI.BorsukNine.FiniteObstruction.c18467 line 393
  46. theorem OAI.BorsukNine.FiniteObstruction.c18468 line 401
  47. theorem OAI.BorsukNine.FiniteObstruction.c18469 line 409
  48. theorem OAI.BorsukNine.FiniteObstruction.c18470 line 417
  49. theorem OAI.BorsukNine.FiniteObstruction.c18471 line 425