OAI/Geometry/Borsuk/FiniteCases/Cases019.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c1644 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c1652 line 16
  3. theorem OAI.BorsukNine.FiniteObstruction.c1653 line 33
  4. theorem OAI.BorsukNine.FiniteObstruction.c1655 line 38
  5. theorem OAI.BorsukNine.FiniteObstruction.c1657 line 43
  6. theorem OAI.BorsukNine.FiniteObstruction.c1659 line 48
  7. theorem OAI.BorsukNine.FiniteObstruction.c1660 line 53
  8. theorem OAI.BorsukNine.FiniteObstruction.c1667 line 70
  9. theorem OAI.BorsukNine.FiniteObstruction.c1668 line 87
  10. theorem OAI.BorsukNine.FiniteObstruction.c1669 line 92
  11. theorem OAI.BorsukNine.FiniteObstruction.c1670 line 109
  12. theorem OAI.BorsukNine.FiniteObstruction.c1671 line 114
  13. theorem OAI.BorsukNine.FiniteObstruction.c1672 line 131
  14. theorem OAI.BorsukNine.FiniteObstruction.c1673 line 136
  15. theorem OAI.BorsukNine.FiniteObstruction.c1674 line 153
  16. theorem OAI.BorsukNine.FiniteObstruction.c1675 line 158
  17. theorem OAI.BorsukNine.FiniteObstruction.c1682 line 175
  18. theorem OAI.BorsukNine.FiniteObstruction.c1684 line 192
  19. theorem OAI.BorsukNine.FiniteObstruction.c1689 line 209
  20. theorem OAI.BorsukNine.FiniteObstruction.c1690 line 214
  21. theorem OAI.BorsukNine.FiniteObstruction.c1697 line 231
  22. theorem OAI.BorsukNine.FiniteObstruction.c1698 line 248
  23. theorem OAI.BorsukNine.FiniteObstruction.c1699 line 253
  24. theorem OAI.BorsukNine.FiniteObstruction.c1700 line 270
  25. theorem OAI.BorsukNine.FiniteObstruction.c1701 line 275
  26. theorem OAI.BorsukNine.FiniteObstruction.c1703 line 292
  27. theorem OAI.BorsukNine.FiniteObstruction.c1704 line 309
  28. theorem OAI.BorsukNine.FiniteObstruction.c1705 line 314
  29. theorem OAI.BorsukNine.FiniteObstruction.c1712 line 331
  30. theorem OAI.BorsukNine.FiniteObstruction.c1715 line 348
  31. theorem OAI.BorsukNine.FiniteObstruction.c1716 line 353
  32. theorem OAI.BorsukNine.FiniteObstruction.c1717 line 370
  33. theorem OAI.BorsukNine.FiniteObstruction.c1719 line 375
  34. theorem OAI.BorsukNine.FiniteObstruction.c1727 line 380
  35. theorem OAI.BorsukNine.FiniteObstruction.c1728 line 397
  36. theorem OAI.BorsukNine.FiniteObstruction.c1729 line 402
  37. theorem OAI.BorsukNine.FiniteObstruction.c1730 line 419
  38. theorem OAI.BorsukNine.FiniteObstruction.c1731 line 424