OAI/Geometry/Borsuk/FiniteCases/Cases072.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c28213 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c28239 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c28240 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c28242 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c28244 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c28263 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c28274 line 69
  8. theorem OAI.BorsukNine.FiniteObstruction.c28278 line 77
  9. theorem OAI.BorsukNine.FiniteObstruction.c28291 line 85
  10. theorem OAI.BorsukNine.FiniteObstruction.c28295 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c28327 line 105
  12. theorem OAI.BorsukNine.FiniteObstruction.c28355 line 115
  13. theorem OAI.BorsukNine.FiniteObstruction.c28379 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c28403 line 135
  15. theorem OAI.BorsukNine.FiniteObstruction.c28404 line 143
  16. theorem OAI.BorsukNine.FiniteObstruction.c28405 line 151
  17. theorem OAI.BorsukNine.FiniteObstruction.c28407 line 159
  18. theorem OAI.BorsukNine.FiniteObstruction.c28408 line 167
  19. theorem OAI.BorsukNine.FiniteObstruction.c28411 line 175
  20. theorem OAI.BorsukNine.FiniteObstruction.c28412 line 183
  21. theorem OAI.BorsukNine.FiniteObstruction.c28413 line 191
  22. theorem OAI.BorsukNine.FiniteObstruction.c28414 line 199
  23. theorem OAI.BorsukNine.FiniteObstruction.c28415 line 207
  24. theorem OAI.BorsukNine.FiniteObstruction.c28416 line 215
  25. theorem OAI.BorsukNine.FiniteObstruction.c28417 line 223
  26. theorem OAI.BorsukNine.FiniteObstruction.c28418 line 231
  27. theorem OAI.BorsukNine.FiniteObstruction.c28419 line 239
  28. theorem OAI.BorsukNine.FiniteObstruction.c28420 line 247
  29. theorem OAI.BorsukNine.FiniteObstruction.c28421 line 255
  30. theorem OAI.BorsukNine.FiniteObstruction.c28423 line 263
  31. theorem OAI.BorsukNine.FiniteObstruction.c28425 line 273
  32. theorem OAI.BorsukNine.FiniteObstruction.c28428 line 283
  33. theorem OAI.BorsukNine.FiniteObstruction.c28431 line 293
  34. theorem OAI.BorsukNine.FiniteObstruction.c28435 line 303
  35. theorem OAI.BorsukNine.FiniteObstruction.c28436 line 313
  36. theorem OAI.BorsukNine.FiniteObstruction.c28443 line 323
  37. theorem OAI.BorsukNine.FiniteObstruction.c28445 line 333
  38. theorem OAI.BorsukNine.FiniteObstruction.c28459 line 343
  39. theorem OAI.BorsukNine.FiniteObstruction.c28461 line 353
  40. theorem OAI.BorsukNine.FiniteObstruction.c28463 line 363
  41. theorem OAI.BorsukNine.FiniteObstruction.c28465 line 373
  42. theorem OAI.BorsukNine.FiniteObstruction.c28467 line 383
  43. theorem OAI.BorsukNine.FiniteObstruction.c28468 line 393
  44. theorem OAI.BorsukNine.FiniteObstruction.c28499 line 403
  45. theorem OAI.BorsukNine.FiniteObstruction.c28502 line 413
  46. theorem OAI.BorsukNine.FiniteObstruction.c28504 line 423