OAI/Geometry/Borsuk/FiniteCases/Cases006.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c475 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c476 line 28
  3. theorem OAI.BorsukNine.FiniteObstruction.c481 line 33
  4. theorem OAI.BorsukNine.FiniteObstruction.c482 line 50
  5. theorem OAI.BorsukNine.FiniteObstruction.c485 line 67
  6. theorem OAI.BorsukNine.FiniteObstruction.c491 line 72
  7. theorem OAI.BorsukNine.FiniteObstruction.c494 line 77
  8. theorem OAI.BorsukNine.FiniteObstruction.c495 line 94
  9. theorem OAI.BorsukNine.FiniteObstruction.c497 line 99
  10. theorem OAI.BorsukNine.FiniteObstruction.c501 line 116
  11. theorem OAI.BorsukNine.FiniteObstruction.c503 line 133
  12. theorem OAI.BorsukNine.FiniteObstruction.c506 line 150
  13. theorem OAI.BorsukNine.FiniteObstruction.c509 line 155
  14. theorem OAI.BorsukNine.FiniteObstruction.c517 line 172
  15. theorem OAI.BorsukNine.FiniteObstruction.c519 line 177
  16. theorem OAI.BorsukNine.FiniteObstruction.c520 line 182
  17. theorem OAI.BorsukNine.FiniteObstruction.c522 line 199
  18. theorem OAI.BorsukNine.FiniteObstruction.c523 line 216
  19. theorem OAI.BorsukNine.FiniteObstruction.c525 line 221
  20. theorem OAI.BorsukNine.FiniteObstruction.c527 line 226
  21. theorem OAI.BorsukNine.FiniteObstruction.c532 line 243
  22. theorem OAI.BorsukNine.FiniteObstruction.c534 line 248
  23. theorem OAI.BorsukNine.FiniteObstruction.c536 line 253
  24. theorem OAI.BorsukNine.FiniteObstruction.c538 line 258
  25. theorem OAI.BorsukNine.FiniteObstruction.c539 line 263
  26. theorem OAI.BorsukNine.FiniteObstruction.c540 line 280
  27. theorem OAI.BorsukNine.FiniteObstruction.c543 line 285
  28. theorem OAI.BorsukNine.FiniteObstruction.c544 line 290
  29. theorem OAI.BorsukNine.FiniteObstruction.c557 line 307
  30. theorem OAI.BorsukNine.FiniteObstruction.c558 line 324
  31. theorem OAI.BorsukNine.FiniteObstruction.c560 line 329
  32. theorem OAI.BorsukNine.FiniteObstruction.c562 line 334
  33. theorem OAI.BorsukNine.FiniteObstruction.c564 line 339
  34. theorem OAI.BorsukNine.FiniteObstruction.c565 line 344
  35. theorem OAI.BorsukNine.FiniteObstruction.c566 line 361
  36. theorem OAI.BorsukNine.FiniteObstruction.c570 line 366
  37. theorem OAI.BorsukNine.FiniteObstruction.c572 line 371
  38. theorem OAI.BorsukNine.FiniteObstruction.c573 line 388
  39. theorem OAI.BorsukNine.FiniteObstruction.c575 line 393
  40. theorem OAI.BorsukNine.FiniteObstruction.c576 line 398
  41. theorem OAI.BorsukNine.FiniteObstruction.c579 line 415
  42. theorem OAI.BorsukNine.FiniteObstruction.c581 line 420
  43. theorem OAI.BorsukNine.FiniteObstruction.c583 line 425