OAI/Geometry/Borsuk/FiniteCases/Cases109.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c32435 line 17
  2. theorem OAI.BorsukNine.FiniteObstruction.c32443 line 26
  3. theorem OAI.BorsukNine.FiniteObstruction.c32446 line 35
  4. theorem OAI.BorsukNine.FiniteObstruction.c32447 line 44
  5. theorem OAI.BorsukNine.FiniteObstruction.c32457 line 53
  6. theorem OAI.BorsukNine.FiniteObstruction.c32460 line 62
  7. theorem OAI.BorsukNine.FiniteObstruction.c32464 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c32467 line 80
  9. theorem OAI.BorsukNine.FiniteObstruction.c32475 line 89
  10. theorem OAI.BorsukNine.FiniteObstruction.c32477 line 98
  11. theorem OAI.BorsukNine.FiniteObstruction.c32479 line 107
  12. theorem OAI.BorsukNine.FiniteObstruction.c32482 line 116
  13. theorem OAI.BorsukNine.FiniteObstruction.c32483 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c32485 line 134
  15. theorem OAI.BorsukNine.FiniteObstruction.c32486 line 143
  16. theorem OAI.BorsukNine.FiniteObstruction.c32487 line 152
  17. theorem OAI.BorsukNine.FiniteObstruction.c32496 line 161
  18. theorem OAI.BorsukNine.FiniteObstruction.c32497 line 170
  19. theorem OAI.BorsukNine.FiniteObstruction.c32505 line 179
  20. theorem OAI.BorsukNine.FiniteObstruction.c32506 line 188
  21. theorem OAI.BorsukNine.FiniteObstruction.c32507 line 197
  22. theorem OAI.BorsukNine.FiniteObstruction.c32516 line 206
  23. theorem OAI.BorsukNine.FiniteObstruction.c32517 line 215
  24. theorem OAI.BorsukNine.FiniteObstruction.c32518 line 224
  25. theorem OAI.BorsukNine.FiniteObstruction.c32521 line 233
  26. theorem OAI.BorsukNine.FiniteObstruction.c32523 line 242
  27. theorem OAI.BorsukNine.FiniteObstruction.c32524 line 251
  28. theorem OAI.BorsukNine.FiniteObstruction.c32525 line 260
  29. theorem OAI.BorsukNine.FiniteObstruction.c32526 line 269
  30. theorem OAI.BorsukNine.FiniteObstruction.c32527 line 278
  31. theorem OAI.BorsukNine.FiniteObstruction.c32534 line 287
  32. theorem OAI.BorsukNine.FiniteObstruction.c32535 line 296
  33. theorem OAI.BorsukNine.FiniteObstruction.c32536 line 305
  34. theorem OAI.BorsukNine.FiniteObstruction.c32537 line 314
  35. theorem OAI.BorsukNine.FiniteObstruction.c32546 line 323
  36. theorem OAI.BorsukNine.FiniteObstruction.c32547 line 332
  37. theorem OAI.BorsukNine.FiniteObstruction.c32549 line 341
  38. theorem OAI.BorsukNine.FiniteObstruction.c32552 line 350
  39. theorem OAI.BorsukNine.FiniteObstruction.c32556 line 359
  40. theorem OAI.BorsukNine.FiniteObstruction.c32557 line 368
  41. theorem OAI.BorsukNine.FiniteObstruction.c32566 line 377
  42. theorem OAI.BorsukNine.FiniteObstruction.c32567 line 386
  43. theorem OAI.BorsukNine.FiniteObstruction.c32568 line 399
  44. theorem OAI.BorsukNine.FiniteObstruction.c32569 line 415