OAI/Geometry/Borsuk/FiniteCases/Cases018.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c1565 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c1566 line 16
  3. theorem OAI.BorsukNine.FiniteObstruction.c1567 line 33
  4. theorem OAI.BorsukNine.FiniteObstruction.c1568 line 38
  5. theorem OAI.BorsukNine.FiniteObstruction.c1569 line 55
  6. theorem OAI.BorsukNine.FiniteObstruction.c1570 line 60
  7. theorem OAI.BorsukNine.FiniteObstruction.c1577 line 77
  8. theorem OAI.BorsukNine.FiniteObstruction.c1578 line 94
  9. theorem OAI.BorsukNine.FiniteObstruction.c1579 line 99
  10. theorem OAI.BorsukNine.FiniteObstruction.c1580 line 116
  11. theorem OAI.BorsukNine.FiniteObstruction.c1581 line 121
  12. theorem OAI.BorsukNine.FiniteObstruction.c1582 line 138
  13. theorem OAI.BorsukNine.FiniteObstruction.c1583 line 143
  14. theorem OAI.BorsukNine.FiniteObstruction.c1584 line 160
  15. theorem OAI.BorsukNine.FiniteObstruction.c1592 line 165
  16. theorem OAI.BorsukNine.FiniteObstruction.c1593 line 182
  17. theorem OAI.BorsukNine.FiniteObstruction.c1594 line 187
  18. theorem OAI.BorsukNine.FiniteObstruction.c1596 line 204
  19. theorem OAI.BorsukNine.FiniteObstruction.c1597 line 221
  20. theorem OAI.BorsukNine.FiniteObstruction.c1598 line 226
  21. theorem OAI.BorsukNine.FiniteObstruction.c1599 line 243
  22. theorem OAI.BorsukNine.FiniteObstruction.c1600 line 248
  23. theorem OAI.BorsukNine.FiniteObstruction.c1608 line 265
  24. theorem OAI.BorsukNine.FiniteObstruction.c1612 line 270
  25. theorem OAI.BorsukNine.FiniteObstruction.c1614 line 275
  26. theorem OAI.BorsukNine.FiniteObstruction.c1622 line 280
  27. theorem OAI.BorsukNine.FiniteObstruction.c1623 line 297
  28. theorem OAI.BorsukNine.FiniteObstruction.c1624 line 302
  29. theorem OAI.BorsukNine.FiniteObstruction.c1625 line 319
  30. theorem OAI.BorsukNine.FiniteObstruction.c1626 line 324
  31. theorem OAI.BorsukNine.FiniteObstruction.c1627 line 341
  32. theorem OAI.BorsukNine.FiniteObstruction.c1628 line 346
  33. theorem OAI.BorsukNine.FiniteObstruction.c1629 line 363
  34. theorem OAI.BorsukNine.FiniteObstruction.c1630 line 368
  35. theorem OAI.BorsukNine.FiniteObstruction.c1637 line 385
  36. theorem OAI.BorsukNine.FiniteObstruction.c1638 line 402
  37. theorem OAI.BorsukNine.FiniteObstruction.c1639 line 407
  38. theorem OAI.BorsukNine.FiniteObstruction.c1643 line 424