OAI/Geometry/Borsuk/FiniteCases/Cases020.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c1732 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c1733 line 16
  3. theorem OAI.BorsukNine.FiniteObstruction.c1734 line 33
  4. theorem OAI.BorsukNine.FiniteObstruction.c1735 line 38
  5. theorem OAI.BorsukNine.FiniteObstruction.c1742 line 55
  6. theorem OAI.BorsukNine.FiniteObstruction.c1743 line 72
  7. theorem OAI.BorsukNine.FiniteObstruction.c1747 line 77
  8. theorem OAI.BorsukNine.FiniteObstruction.c1749 line 82
  9. theorem OAI.BorsukNine.FiniteObstruction.c1750 line 87
  10. theorem OAI.BorsukNine.FiniteObstruction.c1757 line 104
  11. theorem OAI.BorsukNine.FiniteObstruction.c1758 line 121
  12. theorem OAI.BorsukNine.FiniteObstruction.c1759 line 126
  13. theorem OAI.BorsukNine.FiniteObstruction.c1760 line 143
  14. theorem OAI.BorsukNine.FiniteObstruction.c1761 line 148
  15. theorem OAI.BorsukNine.FiniteObstruction.c1763 line 165
  16. theorem OAI.BorsukNine.FiniteObstruction.c1764 line 182
  17. theorem OAI.BorsukNine.FiniteObstruction.c1772 line 187
  18. theorem OAI.BorsukNine.FiniteObstruction.c1774 line 204
  19. theorem OAI.BorsukNine.FiniteObstruction.c1775 line 221
  20. theorem OAI.BorsukNine.FiniteObstruction.c1776 line 226
  21. theorem OAI.BorsukNine.FiniteObstruction.c1778 line 243
  22. theorem OAI.BorsukNine.FiniteObstruction.c1779 line 260
  23. theorem OAI.BorsukNine.FiniteObstruction.c1780 line 265
  24. theorem OAI.BorsukNine.FiniteObstruction.c1787 line 282
  25. theorem OAI.BorsukNine.FiniteObstruction.c1788 line 299
  26. theorem OAI.BorsukNine.FiniteObstruction.c1790 line 304
  27. theorem OAI.BorsukNine.FiniteObstruction.c1791 line 309
  28. theorem OAI.BorsukNine.FiniteObstruction.c1792 line 326
  29. theorem OAI.BorsukNine.FiniteObstruction.c1793 line 331
  30. theorem OAI.BorsukNine.FiniteObstruction.c1794 line 348
  31. theorem OAI.BorsukNine.FiniteObstruction.c1795 line 353
  32. theorem OAI.BorsukNine.FiniteObstruction.c1802 line 370
  33. theorem OAI.BorsukNine.FiniteObstruction.c1803 line 378
  34. theorem OAI.BorsukNine.FiniteObstruction.c1804 line 386
  35. theorem OAI.BorsukNine.FiniteObstruction.c1805 line 394
  36. theorem OAI.BorsukNine.FiniteObstruction.c1806 line 402
  37. theorem OAI.BorsukNine.FiniteObstruction.c1807 line 410
  38. theorem OAI.BorsukNine.FiniteObstruction.c1808 line 418
  39. theorem OAI.BorsukNine.FiniteObstruction.c1809 line 426