OAI/Geometry/Borsuk/FiniteCases/Cases029.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c5867 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c5872 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c5873 line 27
  4. theorem OAI.BorsukNine.FiniteObstruction.c5878 line 35
  5. theorem OAI.BorsukNine.FiniteObstruction.c5881 line 43
  6. theorem OAI.BorsukNine.FiniteObstruction.c5924 line 51
  7. theorem OAI.BorsukNine.FiniteObstruction.c5925 line 61
  8. theorem OAI.BorsukNine.FiniteObstruction.c5932 line 71
  9. theorem OAI.BorsukNine.FiniteObstruction.c5933 line 81
  10. theorem OAI.BorsukNine.FiniteObstruction.c5987 line 91
  11. theorem OAI.BorsukNine.FiniteObstruction.c5995 line 101
  12. theorem OAI.BorsukNine.FiniteObstruction.c6002 line 111
  13. theorem OAI.BorsukNine.FiniteObstruction.c6003 line 119
  14. theorem OAI.BorsukNine.FiniteObstruction.c6004 line 127
  15. theorem OAI.BorsukNine.FiniteObstruction.c6005 line 135
  16. theorem OAI.BorsukNine.FiniteObstruction.c6009 line 143
  17. theorem OAI.BorsukNine.FiniteObstruction.c6012 line 151
  18. theorem OAI.BorsukNine.FiniteObstruction.c6015 line 159
  19. theorem OAI.BorsukNine.FiniteObstruction.c6019 line 167
  20. theorem OAI.BorsukNine.FiniteObstruction.c6021 line 175
  21. theorem OAI.BorsukNine.FiniteObstruction.c6041 line 183
  22. theorem OAI.BorsukNine.FiniteObstruction.c6130 line 193
  23. theorem OAI.BorsukNine.FiniteObstruction.c6143 line 203
  24. theorem OAI.BorsukNine.FiniteObstruction.c6144 line 211
  25. theorem OAI.BorsukNine.FiniteObstruction.c6145 line 219
  26. theorem OAI.BorsukNine.FiniteObstruction.c6149 line 227
  27. theorem OAI.BorsukNine.FiniteObstruction.c6151 line 235
  28. theorem OAI.BorsukNine.FiniteObstruction.c6152 line 243
  29. theorem OAI.BorsukNine.FiniteObstruction.c6157 line 251
  30. theorem OAI.BorsukNine.FiniteObstruction.c6158 line 259
  31. theorem OAI.BorsukNine.FiniteObstruction.c6159 line 267
  32. theorem OAI.BorsukNine.FiniteObstruction.c6161 line 275
  33. theorem OAI.BorsukNine.FiniteObstruction.c6187 line 283
  34. theorem OAI.BorsukNine.FiniteObstruction.c6201 line 293
  35. theorem OAI.BorsukNine.FiniteObstruction.c6229 line 303
  36. theorem OAI.BorsukNine.FiniteObstruction.c6247 line 313
  37. theorem OAI.BorsukNine.FiniteObstruction.c6260 line 323
  38. theorem OAI.BorsukNine.FiniteObstruction.c6283 line 333
  39. theorem OAI.BorsukNine.FiniteObstruction.c6284 line 341
  40. theorem OAI.BorsukNine.FiniteObstruction.c6285 line 349
  41. theorem OAI.BorsukNine.FiniteObstruction.c6288 line 357
  42. theorem OAI.BorsukNine.FiniteObstruction.c6292 line 365
  43. theorem OAI.BorsukNine.FiniteObstruction.c6293 line 373
  44. theorem OAI.BorsukNine.FiniteObstruction.c6294 line 381
  45. theorem OAI.BorsukNine.FiniteObstruction.c6295 line 389
  46. theorem OAI.BorsukNine.FiniteObstruction.c6297 line 397
  47. theorem OAI.BorsukNine.FiniteObstruction.c6303 line 405
  48. theorem OAI.BorsukNine.FiniteObstruction.c6329 line 415
  49. theorem OAI.BorsukNine.FiniteObstruction.c6350 line 425