OAI/Geometry/Borsuk/FiniteCases/Cases062.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c22904 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c22905 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c22907 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c22939 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c22953 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c22959 line 59
  7. theorem OAI.BorsukNine.FiniteObstruction.c22977 line 67
  8. theorem OAI.BorsukNine.FiniteObstruction.c22978 line 77
  9. theorem OAI.BorsukNine.FiniteObstruction.c22987 line 87
  10. theorem OAI.BorsukNine.FiniteObstruction.c23003 line 97
  11. theorem OAI.BorsukNine.FiniteObstruction.c23011 line 107
  12. theorem OAI.BorsukNine.FiniteObstruction.c23039 line 117
  13. theorem OAI.BorsukNine.FiniteObstruction.c23047 line 127
  14. theorem OAI.BorsukNine.FiniteObstruction.c23055 line 137
  15. theorem OAI.BorsukNine.FiniteObstruction.c23071 line 147
  16. theorem OAI.BorsukNine.FiniteObstruction.c23151 line 157
  17. theorem OAI.BorsukNine.FiniteObstruction.c23175 line 167
  18. theorem OAI.BorsukNine.FiniteObstruction.c23197 line 177
  19. theorem OAI.BorsukNine.FiniteObstruction.c23210 line 187
  20. theorem OAI.BorsukNine.FiniteObstruction.c23222 line 197
  21. theorem OAI.BorsukNine.FiniteObstruction.c23226 line 205
  22. theorem OAI.BorsukNine.FiniteObstruction.c23233 line 213
  23. theorem OAI.BorsukNine.FiniteObstruction.c23239 line 221
  24. theorem OAI.BorsukNine.FiniteObstruction.c23273 line 229
  25. theorem OAI.BorsukNine.FiniteObstruction.c23291 line 239
  26. theorem OAI.BorsukNine.FiniteObstruction.c23351 line 249
  27. theorem OAI.BorsukNine.FiniteObstruction.c23352 line 259
  28. theorem OAI.BorsukNine.FiniteObstruction.c23366 line 269
  29. theorem OAI.BorsukNine.FiniteObstruction.c23368 line 277
  30. theorem OAI.BorsukNine.FiniteObstruction.c23370 line 285
  31. theorem OAI.BorsukNine.FiniteObstruction.c23374 line 293
  32. theorem OAI.BorsukNine.FiniteObstruction.c23377 line 301
  33. theorem OAI.BorsukNine.FiniteObstruction.c23413 line 309
  34. theorem OAI.BorsukNine.FiniteObstruction.c23445 line 319
  35. theorem OAI.BorsukNine.FiniteObstruction.c23461 line 329
  36. theorem OAI.BorsukNine.FiniteObstruction.c23465 line 339
  37. theorem OAI.BorsukNine.FiniteObstruction.c23466 line 349
  38. theorem OAI.BorsukNine.FiniteObstruction.c23469 line 359
  39. theorem OAI.BorsukNine.FiniteObstruction.c23475 line 369
  40. theorem OAI.BorsukNine.FiniteObstruction.c23483 line 379
  41. theorem OAI.BorsukNine.FiniteObstruction.c23493 line 389
  42. theorem OAI.BorsukNine.FiniteObstruction.c23496 line 399
  43. theorem OAI.BorsukNine.FiniteObstruction.c23503 line 409
  44. theorem OAI.BorsukNine.FiniteObstruction.c23512 line 417
  45. theorem OAI.BorsukNine.FiniteObstruction.c23515 line 425