OAI/Geometry/Borsuk/FiniteCases/Cases045.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c13996 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c13998 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c14001 line 27
  4. theorem OAI.BorsukNine.FiniteObstruction.c14027 line 35
  5. theorem OAI.BorsukNine.FiniteObstruction.c14039 line 45
  6. theorem OAI.BorsukNine.FiniteObstruction.c14052 line 55
  7. theorem OAI.BorsukNine.FiniteObstruction.c14062 line 65
  8. theorem OAI.BorsukNine.FiniteObstruction.c14078 line 75
  9. theorem OAI.BorsukNine.FiniteObstruction.c14082 line 85
  10. theorem OAI.BorsukNine.FiniteObstruction.c14083 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c14086 line 105
  12. theorem OAI.BorsukNine.FiniteObstruction.c14087 line 115
  13. theorem OAI.BorsukNine.FiniteObstruction.c14095 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c14107 line 135
  15. theorem OAI.BorsukNine.FiniteObstruction.c14109 line 145
  16. theorem OAI.BorsukNine.FiniteObstruction.c14119 line 155
  17. theorem OAI.BorsukNine.FiniteObstruction.c14122 line 165
  18. theorem OAI.BorsukNine.FiniteObstruction.c14123 line 173
  19. theorem OAI.BorsukNine.FiniteObstruction.c14125 line 181
  20. theorem OAI.BorsukNine.FiniteObstruction.c14127 line 189
  21. theorem OAI.BorsukNine.FiniteObstruction.c14130 line 197
  22. theorem OAI.BorsukNine.FiniteObstruction.c14131 line 205
  23. theorem OAI.BorsukNine.FiniteObstruction.c14134 line 213
  24. theorem OAI.BorsukNine.FiniteObstruction.c14139 line 221
  25. theorem OAI.BorsukNine.FiniteObstruction.c14159 line 229
  26. theorem OAI.BorsukNine.FiniteObstruction.c14184 line 239
  27. theorem OAI.BorsukNine.FiniteObstruction.c14192 line 249
  28. theorem OAI.BorsukNine.FiniteObstruction.c14194 line 259
  29. theorem OAI.BorsukNine.FiniteObstruction.c14202 line 269
  30. theorem OAI.BorsukNine.FiniteObstruction.c14203 line 279
  31. theorem OAI.BorsukNine.FiniteObstruction.c14211 line 289
  32. theorem OAI.BorsukNine.FiniteObstruction.c14257 line 299
  33. theorem OAI.BorsukNine.FiniteObstruction.c14262 line 309
  34. theorem OAI.BorsukNine.FiniteObstruction.c14264 line 317
  35. theorem OAI.BorsukNine.FiniteObstruction.c14265 line 325
  36. theorem OAI.BorsukNine.FiniteObstruction.c14266 line 333
  37. theorem OAI.BorsukNine.FiniteObstruction.c14267 line 341
  38. theorem OAI.BorsukNine.FiniteObstruction.c14271 line 349
  39. theorem OAI.BorsukNine.FiniteObstruction.c14274 line 357
  40. theorem OAI.BorsukNine.FiniteObstruction.c14275 line 365
  41. theorem OAI.BorsukNine.FiniteObstruction.c14276 line 373
  42. theorem OAI.BorsukNine.FiniteObstruction.c14277 line 381
  43. theorem OAI.BorsukNine.FiniteObstruction.c14279 line 389
  44. theorem OAI.BorsukNine.FiniteObstruction.c14280 line 397
  45. theorem OAI.BorsukNine.FiniteObstruction.c14281 line 405
  46. theorem OAI.BorsukNine.FiniteObstruction.c14283 line 413
  47. theorem OAI.BorsukNine.FiniteObstruction.c14289 line 423