OAI/Geometry/Borsuk/FiniteCases/Cases103.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c31532 line 14
  2. theorem OAI.BorsukNine.FiniteObstruction.c31533 line 23
  3. theorem OAI.BorsukNine.FiniteObstruction.c31534 line 32
  4. theorem OAI.BorsukNine.FiniteObstruction.c31535 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c31537 line 50
  6. theorem OAI.BorsukNine.FiniteObstruction.c31538 line 65
  7. theorem OAI.BorsukNine.FiniteObstruction.c31548 line 80
  8. theorem OAI.BorsukNine.FiniteObstruction.c31555 line 95
  9. theorem OAI.BorsukNine.FiniteObstruction.c31556 line 110
  10. theorem OAI.BorsukNine.FiniteObstruction.c31557 line 125
  11. theorem OAI.BorsukNine.FiniteObstruction.c31558 line 140
  12. theorem OAI.BorsukNine.FiniteObstruction.c31560 line 155
  13. theorem OAI.BorsukNine.FiniteObstruction.c31563 line 170
  14. theorem OAI.BorsukNine.FiniteObstruction.c31564 line 185
  15. theorem OAI.BorsukNine.FiniteObstruction.c31565 line 200
  16. theorem OAI.BorsukNine.FiniteObstruction.c31572 line 215
  17. theorem OAI.BorsukNine.FiniteObstruction.c31573 line 230
  18. theorem OAI.BorsukNine.FiniteObstruction.c31574 line 245
  19. theorem OAI.BorsukNine.FiniteObstruction.c31576 line 260
  20. theorem OAI.BorsukNine.FiniteObstruction.c31585 line 275
  21. theorem OAI.BorsukNine.FiniteObstruction.c31586 line 290
  22. theorem OAI.BorsukNine.FiniteObstruction.c31587 line 305
  23. theorem OAI.BorsukNine.FiniteObstruction.c31588 line 320
  24. theorem OAI.BorsukNine.FiniteObstruction.c31589 line 335
  25. theorem OAI.BorsukNine.FiniteObstruction.c31594 line 350
  26. theorem OAI.BorsukNine.FiniteObstruction.c31595 line 365
  27. theorem OAI.BorsukNine.FiniteObstruction.c31596 line 380
  28. theorem OAI.BorsukNine.FiniteObstruction.c31597 line 395
  29. theorem OAI.BorsukNine.FiniteObstruction.c31598 line 410
  30. theorem OAI.BorsukNine.FiniteObstruction.c31599 line 425